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

feat(init/setoid): tag equivalence relation

Browse source
This commit is contained in:
Daniel Selsam 2015-12-05 10:10:59 -08:00 committed by Leonardo de Moura
parent fa938bb94c
commit 7a117c45bf
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/setoid.lean
View file

@ -17,12 +17,12 @@ namespace setoid
variable [s : setoid A]
include s
theorem refl (a : A) : a ≈ a :=
theorem refl [refl] (a : A) : a ≈ a :=
and.elim_left (@setoid.iseqv A s) a
theorem symm {a b : A} : a ≈ b → b ≈ a :=
theorem symm [symm] {a b : A} : a ≈ b → b ≈ a :=
λ H, and.elim_left (and.elim_right (@setoid.iseqv A s)) a b H
theorem trans {a b c : A} : a ≈ b → b ≈ c → a ≈ c :=
theorem trans [trans] {a b c : A} : a ≈ b → b ≈ c → a ≈ c :=
λ H₁ H₂, and.elim_right (and.elim_right (@setoid.iseqv A s)) a b c H₁ H₂
end setoid