michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/init/quot): add exists_rep theorem for quotients

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-02 10:52:07 -07:00
parent 1ea56038e3
commit e7448ca77e
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/quot.lean
View file

@ -36,6 +36,9 @@ namespace quot
protected theorem induction_on {A : Type} [s : setoid A] {B : quot s → Prop} (q : quot s) (H : ∀ a, B ⟦a⟧) : B q := protected theorem induction_on {A : Type} [s : setoid A] {B : quot s → Prop} (q : quot s) (H : ∀ a, B ⟦a⟧) : B q :=
ind H q ind H q
theorem exists_rep {A : Type} [s : setoid A] (q : quot s) : ∃ a : A, ⟦a⟧ = q :=
quot.induction_on q (λ a, exists.intro a rfl)
section section
variable {A : Type} variable {A : Type}
variable [s : setoid A] variable [s : setoid A]