Skip to content

Instantly share code, notes, and snippets.

Avatar

Kevin Buzzard kbuzzard

View GitHub Profile
View gist:16e86e94ab7312a8cc9c94281ac3a669
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⟩)
View gist:4adc29a36ca6e8968c390d645729bf3c
-- 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
View gist:b613f9854b110b1df288dabeafaeb105
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
@kbuzzard
kbuzzard / multiset_min.lean
Created Feb 24, 2018
This function computes the min of a multiset.
View multiset_min.lean
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
View gist:50a650e6df7e712138456facb5a81f22
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))
View gist:6f942e335fdf8221f328918b9900ecd7
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*)
View gist:a09dc87e290c0497db65c4c702b37c2f
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
View gist:2a135ef1486fc55c3b4c70ca11cf50b4
[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
View group_axioms_class.lean
-- 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.
View pp.all
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 →