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 i j k l m | |
def empty.elim (A : Sort i) (H : empty) : A := | |
@empty.rec (λ e, A) H | |
def iso0 {A} {C : (empty → A) → Sort i} (f : empty → A) (H : C (empty.elim A)) : C f := | |
eq.rec H (funext (empty.rec _) : empty.elim A = f) | |
def iso1 {A} {C : (unit → A) → Sort i} (f : unit → A) (H : C (λu, f ())) : C f := | |
eq.rec H (funext (λu, unit.rec rfl u) : (λu, f ()) = f) |
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 system.io | |
universes u v | |
namespace hide | |
inductive format.color | |
| red | green | orange | blue | pink | cyan | grey | |
inductive format : Type |
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 w | |
variable {α : Type u} | |
class seq_ty (α : Type u) := | |
(data : Type v) | |
(destruct : data → option (α × data)) | |
structure seq (α : Type u) : Type (max u (v+1)) := | |
(pfx : list α) |
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
/- | |
- Definition of insertion sort. | |
- Copyright Siva Somayyajula, 2017 | |
-/ | |
namespace list | |
universe u | |
variable {α : Type u} |
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 zero_nhd : filter ℚ := | |
lemma mem_zero_nhd {r : ℚ} (h : 0 < r) : {q | abs q < r} ∈ zero_nhd.sets := | |
lemma mem_zero_nhd_le {r : ℚ} (h : 0 < r) : {q | abs q ≤ r} ∈ zero_nhd.sets := | |
lemma mem_zero_nhd_iff {s : set ℚ} : s ∈ zero_nhd.sets ↔ ∃r>0, ∀q:ℚ, abs q < r → q ∈ s := | |
lemma tendsto_zero_nhds {m : α → ℚ} {f : filter α} (hm : ∀r>0, {a | abs (m a) < r} ∈ f.sets) : | |
tendsto m f zero_nhd := | |
lemma pure_zero_le_zero_nhd : pure 0 ≤ zero_nhd := | |
lemma tendsto_neg_rat_zero : tendsto has_neg.neg zero_nhd zero_nhd := | |
lemma tendsto_add_rat_zero : tendsto (λp:ℚ×ℚ, p.1 + p.2) (filter.prod zero_nhd zero_nhd) zero_nhd := | |
lemma tendsto_add_rat_zero' {f g : α → ℚ} {x : filter α} |
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.set.basic tactic.interactive | |
/- | |
Here's Kevin's problem: | |
Let’s say I tell two of my tutees secret non-negative integers, and then I wrote | |
two distinct non-negative integers on my whiteboard; one is the sum of the two | |
secret integers, and the other one is not. I then take it in turns asking my | |
tutees whether they know the other tutee’s number! Prove that eventually one of | |
them will (truthfully) say “yes”. |
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.buffer | |
namespace lean_ir | |
/-- A simple type system based on memory representation -/ | |
inductive type : Type | |
| ptr : type → type -- 4/8 bytes: pointer to data of type X | |
| array : type → type -- (sizeof X)*n bytes for some n: raw array of data of type X | |
| unit : type -- 0 bytes | |
| prod : type → type → type -- unboxed tuple, sizeof X + sizeof Y bytes | |
| bool : type -- 1 byte |
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.option data.list.basic data.int.order | |
attribute [derive decidable_eq] name | |
namespace tc | |
inductive level | |
| var : ℕ → level | |
| zero : level | |
| succ : level → level |
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.finset | |
open nat finset | |
/-- `indep E` is the type of matroids (encoded as systems of independent sets) with ground set `E` : | |
`finset α` -/ | |
structure indep (α : Type*) [decidable_eq α] := | |
(indep : finset (finset α)) | |
-- (I1) | |
(empty_mem_indep : ∅ ∈ indep) | |
-- (I2) |
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
-- presheaf of types basics and equivalence | |
import topology.opens topology.constructions | |
universes u v u₁ v₁ u₂ v₂ | |
open topological_space | |
structure presheaf_of_typesU (X : Type u) [topological_space X] := | |
(F : opens X → Type u) |
OlderNewer