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

library/algebra/complete_lattice): fix typo in comment

Browse source
This commit is contained in:
Jeremy Avigad 2016-01-03 18:21:26 -05:00 committed by Leonardo de Moura
parent 173368801b
commit 7600d04533
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/algebra/complete_lattice.lean
View file

@ -21,14 +21,14 @@ structure complete_lattice [class] (A : Type) extends lattice A :=
(Sup_le : ∀ {b : A} {s : set A} (h : ∀ (a : A), a ∈ s → le a b), le (Sup s) b)
-- Minimal complete_lattice definition based just on Inf.
-- We latet show that complete_lattice_Inf is a complete_lattice
-- We later show that complete_lattice_Inf is a complete_lattice.
structure complete_lattice_Inf [class] (A : Type) extends weak_order A :=
(Inf : set A → A)
(Inf_le : ∀ {a : A} {s : set A}, a ∈ s → le (Inf s) a)
(le_Inf : ∀ {b : A} {s : set A}, (∀ (a : A), a ∈ s → le b a) → le b (Inf s))
-- Minimal complete_lattice definition based just on Sup.
-- We later show that complete_lattice_Sup is a complete_lattice
-- We later show that complete_lattice_Sup is a complete_lattice.
structure complete_lattice_Sup [class] (A : Type) extends weak_order A :=
(Sup : set A → A)
(le_Sup : ∀ {a : A} {s : set A}, a ∈ s → le a (Sup s))