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

refactor(library/init): add auxiliary function mk_equivalence

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-01 17:30:20 -07:00
parent f8023403af
commit 7b64a47221
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/funext.lean
View file

@ -27,7 +27,7 @@ section
λH₁ H₂ x, eq.trans (H₁ x) (H₂ x)
private theorem fun_eqv.is_equivalence (A : Type) (B : A → Type) : equivalence (@fun_eqv A B) :=
and.intro (@fun_eqv.refl A B) (and.intro (@fun_eqv.symm A B) (@fun_eqv.trans A B))
mk_equivalence (@fun_eqv A B) (@fun_eqv.refl A B) (@fun_eqv.symm A B) (@fun_eqv.trans A B)
definition fun_setoid [instance] (A : Type) (B : A → Type) : setoid (Πx : A, B x) :=
setoid.mk (@fun_eqv A B) (fun_eqv.is_equivalence A B)

3
library/init/relation.lean
View file

@ -22,6 +22,9 @@ definition transitive := ∀⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z
definition equivalence := reflexive R ∧ symmetric R ∧ transitive R
definition mk_equivalence (r : reflexive R) (s : symmetric R) (t : transitive R) : equivalence R :=
and.intro r (and.intro s t)
definition irreflexive := ∀x, ¬ x ≺ x
definition anti_symmetric := ∀⦃x y⦄, x ≺ y → y ≺ x → x = y