Collection of miscellaneous finished and unfinished Lean 4 formalizations.
Requires Lake.
git clone https://github.com/mdnestor/MiscLean
cd MiscLean
lake build- Lean homepage: lean-lang.org
- Lean community homepage: leanprover-community.github.io
- Documentation
- Services
- Lean 4 Web - online compiler with mathlib installed
- Loogle - Lean4/Mathlib library search tool
- Lean Zulip chat
- Books
Sample code: proof that composition of surjective functions is surjective.
def surjective {X Y: Type} (f: X → Y): Prop :=
∀ y: Y, ∃ x: X, f x = y
theorem surjective_comp {X Y Z: Type} {f: X → Y} {g: Y → Z}
(hf: surjective f) (hg: surjective g): surjective (g ∘ f) := by
intro z
obtain ⟨y, hy⟩ := hg z
obtain ⟨x, hx⟩ := hf y
exists x
simp [hx, hy]Bonus: proof of Cantor's theorem
def Set (X: Type): Type :=
X → Prop
theorem cantor (f: X → Set X): ¬ surjective f := by
intro h
let S := fun x => ¬ (f x) x
obtain ⟨z, hz⟩ := h S
have: ∀ x: X, S x ↔ ¬ (f x) x := by simp
have := this z
rw [hz] at this
simp_all