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

fix(library/algebra/complete_lattice): avoid looping instances

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-18 16:52:47 -07:00
parent 4787cf179e
commit 65d7c05737
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/algebra/complete_lattice.lean
View file

@ -90,7 +90,7 @@ Sup_le (take x, suppose x ∈ '{a, b},
end complete_lattice_Inf end complete_lattice_Inf
-- Every complete_lattice_Inf is a complete_lattice_Sup -- Every complete_lattice_Inf is a complete_lattice_Sup
definition complete_lattice_Inf_to_complete_lattice_Sup [instance] [C : complete_lattice_Inf A] : complete_lattice_Sup A := definition complete_lattice_Inf_to_complete_lattice_Sup [C : complete_lattice_Inf A] : complete_lattice_Sup A :=
⦃ complete_lattice_Sup, C ⦄ ⦃ complete_lattice_Sup, C ⦄
-- Every complete_lattice_Inf is a complete_lattice -- Every complete_lattice_Inf is a complete_lattice
@ -113,12 +113,15 @@ le_Sup h
end complete_lattice_Sup end complete_lattice_Sup
-- Every complete_lattice_Sup is a complete_lattice_Inf -- Every complete_lattice_Sup is a complete_lattice_Inf
definition complete_lattice_Sup_to_complete_lattice_Inf [instance] [C : complete_lattice_Sup A] : complete_lattice_Inf A := definition complete_lattice_Sup_to_complete_lattice_Inf [C : complete_lattice_Sup A] : complete_lattice_Inf A :=
⦃ complete_lattice_Inf, C ⦄ ⦃ complete_lattice_Inf, C ⦄
-- Every complete_lattice_Sup is a complete_lattice -- Every complete_lattice_Sup is a complete_lattice
section
local attribute complete_lattice_Sup_to_complete_lattice_Inf [instance]
definition complete_lattice_Sup_to_complete_lattice [instance] [C : complete_lattice_Sup A] : complete_lattice A := definition complete_lattice_Sup_to_complete_lattice [instance] [C : complete_lattice_Sup A] : complete_lattice A :=
_ _
end
namespace complete_lattice namespace complete_lattice
variable [C : complete_lattice A] variable [C : complete_lattice A]