| import Mathlib | |
| theorem good_enough (f : ℝ → ℝ) (c : Continuous f) | |
| (onRats : (y : ℚ) → f y ≥ 0) : (x : ℝ) → f x ≥ 0 := | |
| by | |
| by_contra px; push_neg at px; | |
| let ⟨x, hx⟩ := px | |
| let openset := {y : ℝ | y < 0} | |
| have hin : f x ∈ openset := hx | |
| have hio : IsOpen (f ⁻¹' openset) := c.isOpen_preimage openset (isOpen_gt' 0) |
| Claim: there's a bijection between prime ideals of a commutative ring R | |
| (I is a prime ideal of R iff: | |
| (1) (I, +) is a subgroup of (R, +) | |
| (2) if r ∈ R and x ∈ I, then rx ∈ I | |
| (3) if ab ∈ I, then a ∈ I or b ∈ I | |
| (4) 1 ∉ I) | |
| and maps f : R → 2 s.t. | |
| (a) f(0) = 0 |
| module PredArith where | |
| data void : Set where | |
| abort : {A : Set} → void → A | |
| abort () | |
| postulate | |
| ι : Set |
| hg log -r 'FIREFOX_BETA_127_END::FIREFOX_128_0b1_RELEASE' --template "{rev}: {node|short} {date|isodate} {author|person} {desc|firstline}\n" | |
| 820035: 2738f5657419 2024-06-03 14:51 +0000 Mozilla Releng Treescript No bug - tagging 5d25cb332db85c8bb2cda40840be406437ec5e98 with FIREFOX_RELEASE_127_BASE a=release DONTBUILD CLOSED TREE | |
| 823723: f0900bab4570 2024-06-10 14:49 +0000 Mozilla Releng Treescript Merge old head via |hg debugsetparents af9948205327480d29bfcb960d5308ad4a2d0ce7 2738f5657419fba3ece0bc829732f8dfdce7c70a| CLOSED TREE DONTBUILD a=release | |
| 823724: 326824a2c3a7 2024-06-10 14:49 +0000 Mozilla Releng Treescript Preserve old tags after debugsetparents. CLOSED TREE DONTBUILD a=release | |
| 823725: 4926489e7390 2024-06-10 14:49 +0000 Mozilla Releng Treescript No bug - tagging 2738f5657419fba3ece0bc829732f8dfdce7c70a with FIREFOX_BETA_127_END a=release DONTBUILD CLOSED TREE | |
| 823726: 15a675544fcb 2024-06-10 14:49 +0000 Mozilla Releng Treescript no bug - Bumping Firefox l10n changesets r=release a=l10n-bump CLOSED |
| // A quick and dirty lil implementation of the CVM algorithm | |
| // (https://arxiv.org/pdf/2301.10191) | |
| // | |
| // I put Moby Dick (https://www.gutenberg.org/cache/epub/2701/pg2701.txt) | |
| // into /tmp/mb.txt | |
| const fs = require('fs'); | |
| const mb = fs.readFileSync('/tmp/mb.txt', 'utf8') | |
| .replace(/[^a-zA-Z-’]/g, ' ') | |
| .split(/\s+/); |
There is a party with 37 people. Every pair of them is either friends or not friends. Alice and Bob are the only two people at the party with the same number of friends. Alice and Bob are not friends with each other.
How many people are:
| If I have | |
| 𝔹 : ∀X. X → X → X | |
| then parametricity tells me | |
| (b : 𝔹)(f : X → Y)(x₁ x₂ : X) → f (b x₁ x₂) = b (f x₁) (f x₂). | |
| From this I want to prove |
| Suppose ℂ is a ω-cocomplete category: it has colimits of any | |
| diagram that is a functor ω → ℂ. Suppose ℂ has an initial object ⊥. | |
| Suppose F is a functor ℂ → ℂ that preserves all ω-colimits. | |
| Let U : ω → ℂ be the diagram | |
| ! F! F² | |
| ⊥ → F(⊥) → F²(⊥) → ⋯ | |
| Lemma: If we have a map m : FA → A, then we can construct a map colim U → A. |
| open import Agda.Primitive | |
| data ℕ : Set where | |
| zero : ℕ | |
| succ : ℕ → ℕ | |
| record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where | |
| constructor _,_ | |
| field | |
| fst : A |
| Lemma 2: ("Real Induction") Let A be a subset of real numbers. | |
| If | |
| (0) α ∈ A | |
| (1) ∀x ∈ A. ∃y. [x,y) ⊆ A | |
| (2) ∀xy. [x, y) ⊆ A ⇒ y ∈ A | |
| then [α,∞) ⊆ A. | |
| Proof: | |
| Suppose towards a contradiction that [α,∞) ∖ A is nonempty. Set β = inf ([α,∞) ∖ A). | |
| (1) means we can't have β ∈ A, because it would collide with the infimum. |
