Instantly share code, notes, and snippets.

# Kevin Buzzard kbuzzard

Created December 16, 2017 12:55
funny error on line 59
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 import analysis.real def S (a : {n : ℕ // n ≥ 1} → ℝ) (n : ℕ) (H : n ≥ 1) := { r: ℝ | ∃ (m : ℕ) (Hm : m ≥ n), r = a ⟨m,ge_trans Hm H⟩ } noncomputable def a2 : {n : ℕ // n ≥ 1} → ℝ := λ N, 1/N.val def liminf (a : {n : ℕ // n ≥ 1} → ℝ) (linf : ℝ) : Prop := ∃ c : { n : ℕ // n ≥ 1} → ℝ, is_lub { x : ℝ | ∃ (n : ℕ) (H : n ≥ 1), x = c ⟨n,H⟩} linf ∧ ∀ (n : ℕ) (H : n ≥ 1), is_glb (S a n H) (c ⟨n,H⟩)
Created February 4, 2018 02:40
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 -- m and n (the two numbers on the board) are constant. -- The possible worlds are pairs (a,b) of nats with a+b=m or a+b=n structure possible_worlds (m n : ℕ) := (a : ℕ) (b : ℕ) (H : a+b=m ∨ a+b=n) open nat -- the predicate "beliefs m n t" represents the beliefs (i.e. opinions of the
Created February 23, 2018 20:26
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 def extended_le : option ℕ → option ℕ → Prop | _ none := true | none (some n) := false | (some m) (some n) := m ≤ n instance : has_le (option ℕ) := ⟨extended_le⟩ lemma none_le_none : (none : option ℕ) ≤ none := trivial lemma some_le_none (m : ℕ) : (some m) ≤ none := trivial
Created February 24, 2018 01:06
This function computes the min of a multiset.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 import data.multiset def extended_le : option ℕ → option ℕ → Prop | _ none := true | none (some n) := false | (some m) (some n) := m ≤ n instance : has_le (option ℕ) := ⟨extended_le⟩ lemma none_le_none : (none : option ℕ) ≤ none := trivial
Created March 5, 2018 08:41
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 import analysis.topology.continuity universes u v local attribute [class] topological_space.is_open structure presheaf_of_types (α : Type*) [T : topological_space α] := (F : Π U : set α, T.is_open U → Type*) (res : ∀ (U V : set α) (OU : T.is_open U) (OV : T.is_open V) (H : V ⊆ U), (F U OU) → (F V OV))
Created March 5, 2018 08:54
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 universes u v theorem set.subset.trans {α : Type*} {a b c : set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c := assume x h, bc (ab h) def set.preimage {α : Type u} {β : Type v} (f : α → β) (s : set β) : set α := {x | f x ∈ s} infix ` ⁻¹' `:80 := set.preimage structure presheaf_of_types (α : Type*) := (F : Π U : set α, Type*)
Created April 20, 2018 17:44
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 goal before show (apply_instance fails) ⊢ @is_ring_hom.{u u} R (@localization.away.{u} (@localization.loc.{u} R _inst_1 (@powers.{u} R (@ring.to_monoid.{u} R (@comm_ring.to_ring.{u} R _inst_1)) f) (@powers.is_submonoid.{u} R (@ring.to_monoid.{u} R (@comm_ring.to_ring.{u} R _inst_1)) f)) (@localization.comm_ring.{u} R _inst_1 (@powers.{u} R (@ring.to_monoid.{u} R (@comm_ring.to_ring.{u} R _inst_1)) f) (@powers.is_submonoid.{u} R (@ring.to_monoid.{u} R (@comm_ring.to_ring.{u} R _inst_1)) f)) (@localization.of_comm_ring.{u} R _inst_1
Created April 24, 2018 16:36
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 [class_instances] class-instance resolution trace [class_instances] (0) ?x_0 : comm_ring (@loc (@loc R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _) (@localization.comm_ring R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _) (@powers (@loc R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _) (@ring.to_monoid (@loc R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _) (@comm_ring.to_ring (@loc R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _) (@localization.comm_ring R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _))) g) _) := _inst_6
Created April 28, 2018 16:42
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 -- do I use a section? What even is a section? -- so I use a namespace? What would a sensible convention be? -- I don't care about junk like imports at the beginning of files -- I am trying to write down a really uncluttered proof that -- one of the axioms that Lean uses to define a group -- actually follows from the others. -- We will build a structure modelling groups as defined by Lean, minus the axiom mul_one.
Created May 20, 2018 17:03
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 X : Type u, _inst_1 : topological_space.{u} X, B : set.{u} (set.{u} X), HB : @topological_space.is_topological_basis.{u} X _inst_1 B, FPRB : @presheaf_of_rings_on_basis.{u} X _inst_1 B HB, x : X, Hstandard : ∀ (U V : set.{u} X), @has_mem.mem.{u u} (set.{u} X) (set.{u} (set.{u} X)) (@set.has_mem.{u} (set.{u} X)) U B → @has_mem.mem.{u u} (set.{u} X) (set.{u} (set.{u} X)) (@set.has_mem.{u} (set.{u} X)) V B →