From 7600d045337a7ce0545bdc4dcd1b86e947063994 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 3 Jan 2016 18:21:26 -0500 Subject: [PATCH] library/algebra/complete_lattice): fix typo in comment --- library/algebra/complete_lattice.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/algebra/complete_lattice.lean b/library/algebra/complete_lattice.lean index d4ddbf07f6..e10e094f08 100644 --- a/library/algebra/complete_lattice.lean +++ b/library/algebra/complete_lattice.lean @@ -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))