refactor(library/algebra/complete_lattice): make complete lattices more usable
I addressed two problems. First, the theorem names and notation were all in the namespace complete_lattice. The problem was that if you opened that namespace, names (like "sup" and "inf") and notation clashed with global notation for lattices. The other problem was that if you defined a lattice using Sup, the Sup you got was not the Sup you want; it was the Sup-construction from the Inf-construction from the Sup. Everything seems good now.
This commit is contained in:
parent
7fe71c972f
commit
a08395b17e
1 changed files with 77 additions and 9 deletions
|
@ -20,6 +20,26 @@ structure complete_lattice [class] (A : Type) extends lattice A :=
|
||||||
(le_Sup : ∀ {a : A} {s : set A}, a ∈ s → le a (Sup s))
|
(le_Sup : ∀ {a : A} {s : set A}, a ∈ s → le a (Sup s))
|
||||||
(Sup_le : ∀ {b : A} {s : set A} (h : ∀ (a : A), a ∈ s → le a b), le (Sup s) b)
|
(Sup_le : ∀ {b : A} {s : set A} (h : ∀ (a : A), a ∈ s → le a b), le (Sup s) b)
|
||||||
|
|
||||||
|
section
|
||||||
|
variable [complete_lattice A]
|
||||||
|
|
||||||
|
definition Inf (S : set A) : A := complete_lattice.Inf S
|
||||||
|
prefix `⨅ `:70 := Inf
|
||||||
|
|
||||||
|
definition Sup (S : set A) : A := complete_lattice.Sup S
|
||||||
|
prefix `⨆ `:65 := Sup
|
||||||
|
|
||||||
|
theorem Inf_le {a : A} {s : set A} (H : a ∈ s) : (Inf s) ≤ a := complete_lattice.Inf_le H
|
||||||
|
|
||||||
|
theorem le_Inf {b : A} {s : set A} (H : ∀ (a : A), a ∈ s → b ≤ a) : b ≤ Inf s :=
|
||||||
|
complete_lattice.le_Inf H
|
||||||
|
|
||||||
|
theorem le_Sup {a : A} {s : set A} (H : a ∈ s) : a ≤ Sup s := complete_lattice.le_Sup H
|
||||||
|
|
||||||
|
theorem Sup_le {b : A} {s : set A} (H : ∀ (a : A), a ∈ s → a ≤ b) : Sup s ≤ b :=
|
||||||
|
complete_lattice.Sup_le H
|
||||||
|
end
|
||||||
|
|
||||||
-- Minimal complete_lattice definition based just on Inf.
|
-- Minimal complete_lattice definition based just on Inf.
|
||||||
-- We later 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 :=
|
structure complete_lattice_Inf [class] (A : Type) extends weak_order A :=
|
||||||
|
@ -93,7 +113,8 @@ definition complete_lattice_Inf_to_complete_lattice_Sup [C : complete_lattice_In
|
||||||
⦃ complete_lattice_Sup, C ⦄
|
⦃ complete_lattice_Sup, C ⦄
|
||||||
|
|
||||||
-- Every complete_lattice_Inf is a complete_lattice
|
-- Every complete_lattice_Inf is a complete_lattice
|
||||||
definition complete_lattice_Inf_to_complete_lattice [instance] [C : complete_lattice_Inf A] : complete_lattice A :=
|
definition complete_lattice_Inf_to_complete_lattice [trans_instance] [reducible] [C : complete_lattice_Inf A] :
|
||||||
|
complete_lattice A :=
|
||||||
⦃ complete_lattice, C ⦄
|
⦃ complete_lattice, C ⦄
|
||||||
|
|
||||||
namespace complete_lattice_Sup
|
namespace complete_lattice_Sup
|
||||||
|
@ -109,26 +130,63 @@ suppose a ∈ s, Sup_le
|
||||||
|
|
||||||
lemma le_Inf {b : A} {s : set A} (h : ∀ (a : A), a ∈ s → b ≤ a) : b ≤ Inf s :=
|
lemma le_Inf {b : A} {s : set A} (h : ∀ (a : A), a ∈ s → b ≤ a) : b ≤ Inf s :=
|
||||||
le_Sup h
|
le_Sup h
|
||||||
|
|
||||||
|
local prefix `⨅`:70 := Inf
|
||||||
|
local prefix `⨆`:65 := Sup
|
||||||
|
|
||||||
|
definition inf (a b : A) := ⨅ '{a, b}
|
||||||
|
definition sup (a b : A) := ⨆ '{a, b}
|
||||||
|
|
||||||
|
local infix `⊓` := inf
|
||||||
|
local infix `⊔` := sup
|
||||||
|
|
||||||
|
lemma inf_le_left (a b : A) : a ⊓ b ≤ a :=
|
||||||
|
Inf_le !mem_insert
|
||||||
|
|
||||||
|
lemma inf_le_right (a b : A) : a ⊓ b ≤ b :=
|
||||||
|
Inf_le (!mem_insert_of_mem !mem_insert)
|
||||||
|
|
||||||
|
lemma le_inf {a b c : A} : c ≤ a → c ≤ b → c ≤ a ⊓ b :=
|
||||||
|
assume h₁ h₂,
|
||||||
|
le_Inf (take x, suppose x ∈ '{a, b},
|
||||||
|
or.elim (eq_or_mem_of_mem_insert this)
|
||||||
|
(suppose x = a, begin subst x, exact h₁ end)
|
||||||
|
(suppose x ∈ '{b},
|
||||||
|
assert x = b, from !eq_of_mem_singleton this,
|
||||||
|
begin subst x, exact h₂ end))
|
||||||
|
|
||||||
|
lemma le_sup_left (a b : A) : a ≤ a ⊔ b :=
|
||||||
|
le_Sup !mem_insert
|
||||||
|
|
||||||
|
lemma le_sup_right (a b : A) : b ≤ a ⊔ b :=
|
||||||
|
le_Sup (!mem_insert_of_mem !mem_insert)
|
||||||
|
|
||||||
|
lemma sup_le {a b c : A} : a ≤ c → b ≤ c → a ⊔ b ≤ c :=
|
||||||
|
assume h₁ h₂,
|
||||||
|
Sup_le (take x, suppose x ∈ '{a, b},
|
||||||
|
or.elim (eq_or_mem_of_mem_insert this)
|
||||||
|
(assume H : x = a, by subst x; exact h₁)
|
||||||
|
(suppose x ∈ '{b},
|
||||||
|
assert x = b, from !eq_of_mem_singleton this,
|
||||||
|
by subst x; exact 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 [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
|
section
|
||||||
local attribute complete_lattice_Sup_to_complete_lattice_Inf [instance]
|
definition complete_lattice_Sup_to_complete_lattice [trans_instance] [reducible] [C : complete_lattice_Sup A] :
|
||||||
definition complete_lattice_Sup_to_complete_lattice [instance] [C : complete_lattice_Sup A] : complete_lattice A :=
|
complete_lattice A :=
|
||||||
_
|
⦃ complete_lattice, C ⦄
|
||||||
end
|
end
|
||||||
|
|
||||||
namespace complete_lattice
|
section complete_lattice
|
||||||
variable [C : complete_lattice A]
|
variable [C : complete_lattice A]
|
||||||
include C
|
include C
|
||||||
prefix `⨅`:70 := Inf
|
|
||||||
prefix `⨆`:65 := Sup
|
|
||||||
infix ` ⊓ ` := inf
|
|
||||||
infix ` ⊔ ` := sup
|
|
||||||
|
|
||||||
variable {f : A → A}
|
variable {f : A → A}
|
||||||
premise (mono : ∀ x y : A, x ≤ y → f x ≤ f y)
|
premise (mono : ∀ x y : A, x ≤ y → f x ≤ f y)
|
||||||
|
@ -178,6 +236,8 @@ have h₂ : ∀ b, f b = b → b ≤ a, from
|
||||||
le_Sup this,
|
le_Sup this,
|
||||||
exists.intro a (and.intro h₁ h₂)
|
exists.intro a (and.intro h₁ h₂)
|
||||||
|
|
||||||
|
/- top and bot -/
|
||||||
|
|
||||||
definition bot : A := ⨅ univ
|
definition bot : A := ⨅ univ
|
||||||
definition top : A := ⨆ univ
|
definition top : A := ⨆ univ
|
||||||
notation `⊥` := bot
|
notation `⊥` := bot
|
||||||
|
@ -199,6 +259,8 @@ assume h,
|
||||||
have ⊤ ≤ a, from Sup_le (take b bin, h b),
|
have ⊤ ≤ a, from Sup_le (take b bin, h b),
|
||||||
le.antisymm !le_top this
|
le.antisymm !le_top this
|
||||||
|
|
||||||
|
/- general facts about complete lattices -/
|
||||||
|
|
||||||
lemma Inf_singleton {a : A} : ⨅'{a} = a :=
|
lemma Inf_singleton {a : A} : ⨅'{a} = a :=
|
||||||
have ⨅'{a} ≤ a, from
|
have ⨅'{a} ≤ a, from
|
||||||
Inf_le !mem_insert,
|
Inf_le !mem_insert,
|
||||||
|
@ -269,6 +331,12 @@ have le₂ : ⨅ univ ≤ ⨆ (∅ : set A), from
|
||||||
Inf_le !mem_univ,
|
Inf_le !mem_univ,
|
||||||
le.antisymm le₁ le₂
|
le.antisymm le₁ le₂
|
||||||
|
|
||||||
|
lemma Sup_pair (a b : A) : Sup '{a, b} = sup a b :=
|
||||||
|
by rewrite [insert_eq, Sup_union, *Sup_singleton]
|
||||||
|
|
||||||
|
lemma Inf_pair (a b : A) : Inf '{a, b} = inf a b :=
|
||||||
|
by rewrite [insert_eq, Inf_union, *Inf_singleton]
|
||||||
|
|
||||||
end complete_lattice
|
end complete_lattice
|
||||||
|
|
||||||
/- complete lattice instances -/
|
/- complete lattice instances -/
|
||||||
|
|
Loading…
Reference in a new issue