refactor(library/data/set/filter): get filters working with complete lattice notation
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
a08395b17e
commit
41342f53df
1 changed files with 247 additions and 169 deletions
|
|
@ -1,7 +1,7 @@
|
||||||
/-
|
/-
|
||||||
Copyright (c) 2015 Jeremy Avigad. All rights reserved.
|
Copyright (c) 2015 Jeremy Avigad. All rights reserved.
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Author: Jeremy Avigad
|
Authors: Jeremy Avigad, Jacob Gross
|
||||||
|
|
||||||
Filters, following Hölzl, Immler, and Huffman, "Type classes and filters for mathematical
|
Filters, following Hölzl, Immler, and Huffman, "Type classes and filters for mathematical
|
||||||
analysis in Isabelle/HOL".
|
analysis in Isabelle/HOL".
|
||||||
|
|
@ -44,6 +44,16 @@ theorem eventually_and (H₁ : eventually P F) (H₂ : eventually Q F) :
|
||||||
eventually (λ x, P x ∧ Q x) F :=
|
eventually (λ x, P x ∧ Q x) F :=
|
||||||
!filter.inter_closed H₁ H₂
|
!filter.inter_closed H₁ H₂
|
||||||
|
|
||||||
|
theorem eventually_of_eventually_and_left {P Q : A → Prop} {F : filter A}
|
||||||
|
(H : eventually (λ x, P x ∧ Q x) F) :
|
||||||
|
eventually P F :=
|
||||||
|
!filter.is_mono (λ x HPQ, and.elim_left HPQ) H
|
||||||
|
|
||||||
|
theorem eventually_of_eventually_and_right {P Q : A → Prop} {F : filter A}
|
||||||
|
(H : eventually (λ x, P x ∧ Q x) F) :
|
||||||
|
eventually Q F :=
|
||||||
|
!filter.is_mono (λ x HPQ, and.elim_right HPQ) H
|
||||||
|
|
||||||
theorem eventually_mp (H₁ : eventually (λx, P x → Q x) F) (H₂ : eventually P F) :
|
theorem eventually_mp (H₁ : eventually (λx, P x → Q x) F) (H₂ : eventually P F) :
|
||||||
eventually Q F :=
|
eventually Q F :=
|
||||||
have ∀ x, (P x → Q x) ∧ P x → Q x, from take x, assume H, and.left H (and.right H),
|
have ∀ x, (P x → Q x) ∧ P x → Q x, from take x, assume H, and.left H (and.right H),
|
||||||
|
|
@ -85,8 +95,6 @@ eventually_mono (eventually_and H₁ H₂) (λ x H, iff.mpr (and.left H) (and.ri
|
||||||
theorem eventually_iff_iff (H : eventually (λ x, P x ↔ Q x) F) : eventually P F ↔ eventually Q F :=
|
theorem eventually_iff_iff (H : eventually (λ x, P x ↔ Q x) F) : eventually P F ↔ eventually Q F :=
|
||||||
iff.intro (eventually_iff_mp H) (eventually_iff_mpr H)
|
iff.intro (eventually_iff_mp H) (eventually_iff_mpr H)
|
||||||
|
|
||||||
-- TODO: port frequently and properties?
|
|
||||||
|
|
||||||
/- filters form a lattice under ⊇ -/
|
/- filters form a lattice under ⊇ -/
|
||||||
|
|
||||||
protected theorem eq : sets F₁ = sets F₂ → F₁ = F₂ :=
|
protected theorem eq : sets F₁ = sets F₂ → F₁ = F₂ :=
|
||||||
|
|
@ -96,30 +104,231 @@ begin
|
||||||
subst s₁, intros, exact rfl
|
subst s₁, intros, exact rfl
|
||||||
end
|
end
|
||||||
|
|
||||||
definition weakens [reducible] (F₁ F₂ : filter A) := F₁ ⊇ F₂
|
namespace complete_lattice
|
||||||
infix `≼`:50 := weakens
|
definition le [reducible] (F₁ F₂ : filter A) := F₁ ⊇ F₂
|
||||||
|
local infix `≤`:50 := le
|
||||||
|
|
||||||
definition refines [reducible] (F₁ F₂ : filter A) := F₁ ⊆ F₂
|
definition ge [reducible] (F₁ F₂ : filter A) := F₁ ⊆ F₂
|
||||||
infix `≽`:50 := refines
|
local infix `≥`:50 := ge
|
||||||
|
|
||||||
theorem weakens.refl (F : filter A) : F ≼ F := subset.refl _
|
theorem le_refl (F : filter A) : F ≤ F := subset.refl _
|
||||||
|
|
||||||
theorem weakens.trans {F₁ F₂ F₃ : filter A} (H₁ : F₁ ≼ F₂) (H₂ : F₂ ≼ F₃) : F₁ ≼ F₃ :=
|
theorem le_trans {F₁ F₂ F₃ : filter A} (H₁ : F₁ ≤ F₂) (H₂ : F₂ ≤ F₃) : F₁ ≤ F₃ :=
|
||||||
subset.trans H₂ H₁
|
subset.trans H₂ H₁
|
||||||
|
|
||||||
theorem weakens.antisymm (H₁ : F₁ ≼ F₂) (H₂ : F₂ ≼ F₁) : F₁ = F₂ :=
|
theorem le_antisymm (H₁ : F₁ ≤ F₂) (H₂ : F₂ ≤ F₁) : F₁ = F₂ :=
|
||||||
filter.eq (eq_of_subset_of_subset H₂ H₁)
|
filter.eq (eq_of_subset_of_subset H₂ H₁)
|
||||||
|
|
||||||
definition bot : filter A :=
|
definition sup (F₁ F₂ : filter A) : filter A :=
|
||||||
|
⦃ filter,
|
||||||
|
sets := F₁ ∩ F₂,
|
||||||
|
univ_mem_sets := and.intro (filter.univ_mem_sets F₁) (filter.univ_mem_sets F₂),
|
||||||
|
inter_closed := abstract
|
||||||
|
λ a b Ha Hb,
|
||||||
|
and.intro
|
||||||
|
(filter.inter_closed F₁ (and.left Ha) (and.left Hb))
|
||||||
|
(filter.inter_closed F₂ (and.right Ha) (and.right Hb))
|
||||||
|
end,
|
||||||
|
is_mono := abstract
|
||||||
|
λ a b Hsub Ha,
|
||||||
|
and.intro
|
||||||
|
(filter.is_mono F₁ Hsub (and.left Ha))
|
||||||
|
(filter.is_mono F₂ Hsub (and.right Ha))
|
||||||
|
end
|
||||||
|
⦄
|
||||||
|
local infix ` ⊔ `:65 := sup
|
||||||
|
|
||||||
|
definition inf (F₁ F₂ : filter A) : filter A :=
|
||||||
|
⦃ filter,
|
||||||
|
sets := {r | ∃₀ s ∈ F₁, ∃₀ t ∈ F₂, r ⊇ s ∩ t},
|
||||||
|
univ_mem_sets := abstract
|
||||||
|
bounded_exists.intro (univ_mem_sets F₁)
|
||||||
|
(bounded_exists.intro (univ_mem_sets F₂)
|
||||||
|
(by rewrite univ_inter; apply subset.refl))
|
||||||
|
end,
|
||||||
|
inter_closed := abstract
|
||||||
|
λ a b Ha Hb,
|
||||||
|
obtain a₁ [a₁F₁ [a₂ [a₂F₂ (Ha' : a ⊇ a₁ ∩ a₂)]]], from Ha,
|
||||||
|
obtain b₁ [b₁F₁ [b₂ [b₂F₂ (Hb' : b ⊇ b₁ ∩ b₂)]]], from Hb,
|
||||||
|
assert a₁ ∩ b₁ ∩ (a₂ ∩ b₂) = a₁ ∩ a₂ ∩ (b₁ ∩ b₂),
|
||||||
|
by rewrite [*inter_assoc, inter_left_comm b₁],
|
||||||
|
have a ∩ b ⊇ a₁ ∩ b₁ ∩ (a₂ ∩ b₂),
|
||||||
|
begin
|
||||||
|
rewrite this,
|
||||||
|
apply subset_inter,
|
||||||
|
{apply subset.trans,
|
||||||
|
apply inter_subset_left,
|
||||||
|
exact Ha'},
|
||||||
|
apply subset.trans,
|
||||||
|
apply inter_subset_right,
|
||||||
|
exact Hb'
|
||||||
|
end,
|
||||||
|
bounded_exists.intro (inter_closed F₁ a₁F₁ b₁F₁)
|
||||||
|
(bounded_exists.intro (inter_closed F₂ a₂F₂ b₂F₂)
|
||||||
|
this)
|
||||||
|
end,
|
||||||
|
is_mono := abstract
|
||||||
|
λ a b Hsub Ha,
|
||||||
|
obtain a₁ [a₁F₁ [a₂ [a₂F₂ (Ha' : a ⊇ a₁ ∩ a₂)]]], from Ha,
|
||||||
|
bounded_exists.intro a₁F₁
|
||||||
|
(bounded_exists.intro a₂F₂ (subset.trans Ha' Hsub))
|
||||||
|
end
|
||||||
|
⦄
|
||||||
|
infix `⊓`:70 := inf
|
||||||
|
|
||||||
|
definition Sup (S : set (filter A)) : filter A :=
|
||||||
|
⦃ filter,
|
||||||
|
sets := ⋂ F ∈ S, sets F,
|
||||||
|
univ_mem_sets := λ F FS, univ_mem_sets F,
|
||||||
|
inter_closed := abstract
|
||||||
|
λ a b Ha Hb F FS,
|
||||||
|
inter_closed F (Ha F FS) (Hb F FS)
|
||||||
|
end,
|
||||||
|
is_mono := abstract
|
||||||
|
λ a b asubb Ha F FS,
|
||||||
|
is_mono F asubb (Ha F FS)
|
||||||
|
end
|
||||||
|
⦄
|
||||||
|
local prefix `⨆ `:65 := Sup
|
||||||
|
|
||||||
|
definition Inf (S : set (filter A)) : filter A :=
|
||||||
|
Sup {F | ∀ G, G ∈ S → G ≥ F}
|
||||||
|
|
||||||
|
local prefix `⨅ `:70 := Inf
|
||||||
|
|
||||||
|
theorem le_sup_left (F₁ F₂ : filter A) : F₁ ≤ F₁ ⊔ F₂ :=
|
||||||
|
inter_subset_left _ _
|
||||||
|
|
||||||
|
theorem le_sup_right (F₁ F₂ : filter A) : F₂ ≤ F₁ ⊔ F₂ :=
|
||||||
|
inter_subset_right _ _
|
||||||
|
|
||||||
|
theorem sup_le (H₁ : F₁ ≤ F) (H₂ : F₂ ≤ F) : F₁ ⊔ F₂ ≤ F :=
|
||||||
|
subset_inter H₁ H₂
|
||||||
|
|
||||||
|
theorem inf_le_left (F₁ F₂ : filter A) : F₁ ⊓ F₂ ≤ F₁ :=
|
||||||
|
take s, suppose s ∈ F₁,
|
||||||
|
bounded_exists.intro `s ∈ F₁`
|
||||||
|
(bounded_exists.intro (univ_mem_sets F₂) (by rewrite inter_univ; apply subset.refl))
|
||||||
|
|
||||||
|
theorem inf_le_right (F₁ F₂ : filter A) : F₁ ⊓ F₂ ≤ F₂ :=
|
||||||
|
take s, suppose s ∈ F₂,
|
||||||
|
bounded_exists.intro (univ_mem_sets F₁)
|
||||||
|
(bounded_exists.intro `s ∈ F₂` (by rewrite univ_inter; apply subset.refl))
|
||||||
|
|
||||||
|
theorem le_inf (H₁ : F ≤ F₁) (H₂ : F ≤ F₂) : F ≤ F₁ ⊓ F₂ :=
|
||||||
|
take s : set A, suppose (s ∈ (F₁ ⊓ F₂ : set (set A))),
|
||||||
|
obtain a₁ [a₁F₁ [a₂ [a₂F₂ (Hsub : s ⊇ a₁ ∩ a₂)]]], from this,
|
||||||
|
have a₁ ∈ F, from H₁ a₁F₁,
|
||||||
|
have a₂ ∈ F, from H₂ a₂F₂,
|
||||||
|
show s ∈ F, from is_mono F Hsub (inter_closed F `a₁ ∈ F` `a₂ ∈ F`)
|
||||||
|
|
||||||
|
theorem Sup_le {F : filter A} {S : set (filter A)} (H : ∀₀ G ∈ S, G ≤ F) : ⨆ S ≤ F :=
|
||||||
|
λ s Fs G GS, H GS Fs
|
||||||
|
|
||||||
|
theorem le_Sup {F : filter A} {S : set (filter A)} (FS : F ∈ S) : F ≤ ⨆ S :=
|
||||||
|
λ s sInfS, sInfS F FS
|
||||||
|
|
||||||
|
theorem le_Inf {F : filter A} {S : set (filter A)} (H : ∀₀ G ∈ S, F ≤ G) : F ≤ ⨅ S :=
|
||||||
|
le_Sup H
|
||||||
|
|
||||||
|
theorem Inf_le {F : filter A} {S : set (filter A)} (FS : F ∈ S) : ⨅ S ≤ F :=
|
||||||
|
Sup_le (λ G GS, GS F FS)
|
||||||
|
end complete_lattice
|
||||||
|
|
||||||
|
protected definition complete_lattice [reducible] [trans_instance] : complete_lattice (filter A) :=
|
||||||
|
⦃ complete_lattice,
|
||||||
|
le := complete_lattice.le,
|
||||||
|
le_refl := complete_lattice.le_refl,
|
||||||
|
le_trans := @complete_lattice.le_trans A,
|
||||||
|
le_antisymm := @complete_lattice.le_antisymm A,
|
||||||
|
inf := complete_lattice.inf,
|
||||||
|
le_inf := @complete_lattice.le_inf A,
|
||||||
|
inf_le_left := @complete_lattice.inf_le_left A,
|
||||||
|
inf_le_right := @complete_lattice.inf_le_right A,
|
||||||
|
sup := complete_lattice.sup,
|
||||||
|
sup_le := @complete_lattice.sup_le A,
|
||||||
|
le_sup_left := complete_lattice.le_sup_left,
|
||||||
|
le_sup_right := complete_lattice.le_sup_right,
|
||||||
|
Inf := complete_lattice.Inf,
|
||||||
|
Inf_le := @complete_lattice.Inf_le A,
|
||||||
|
le_Inf := @complete_lattice.le_Inf A,
|
||||||
|
Sup := complete_lattice.Sup,
|
||||||
|
Sup_le := @complete_lattice.Sup_le A,
|
||||||
|
le_Sup := @complete_lattice.le_Sup A
|
||||||
|
⦄
|
||||||
|
|
||||||
|
protected theorem le_of_subset {F₁ F₂ : filter A} (H : F₁ ≤ F₂) : sets F₂ ⊆ sets F₁ := H
|
||||||
|
|
||||||
|
protected theorem subset_of_le {F₁ F₂ : filter A} (H : sets F₂ ⊆ sets F₁) : F₁ ≤ F₂ := H
|
||||||
|
|
||||||
|
theorem sets_Sup (S : set (filter A)) : sets (⨆ S) = ⋂ F ∈ S, sets F := rfl
|
||||||
|
|
||||||
|
theorem sets_sup (F₁ F₂ : filter A) : sets (F₁ ⊔ F₂) = sets F₁ ∩ sets F₂ := rfl
|
||||||
|
|
||||||
|
theorem sets_inf (F₁ F₂ : filter A) : sets (F₁ ⊓ F₂) = {r | ∃₀ s ∈ F₁, ∃₀ t ∈ F₂, r ⊇ s ∩ t} := rfl
|
||||||
|
|
||||||
|
/- eventually and lattice operations -/
|
||||||
|
|
||||||
|
theorem eventually_of_le (H₁ : eventually P F₁) (H₂ : F₂ ≤ F₁) : eventually P F₂ :=
|
||||||
|
filter.subset_of_le H₂ H₁
|
||||||
|
|
||||||
|
theorem le_of_forall_eventually (H : ∀ P, eventually P F₁ → eventually P F₂) : F₂ ≤ F₁ := H
|
||||||
|
|
||||||
|
theorem eventually_Sup_iff (P : A → Prop) (S : set (filter A)) :
|
||||||
|
eventually P (⨆ S) ↔ ∀₀ F ∈ S, eventually P F :=
|
||||||
|
by rewrite [↑eventually, sets_Sup]
|
||||||
|
|
||||||
|
theorem eventually_Sup {P : A → Prop} {S : set (filter A)} (H : ∀₀ F ∈ S, eventually P F) :
|
||||||
|
eventually P (⨆ S) :=
|
||||||
|
iff.mpr (eventually_Sup_iff P S) H
|
||||||
|
|
||||||
|
theorem eventually_of_eventually_Sup {P : A → Prop} {S : set (filter A)}
|
||||||
|
(H : eventually P (⨆ S)) {F : filter A} (FS : F ∈ S) :
|
||||||
|
eventually P F :=
|
||||||
|
iff.mp (eventually_Sup_iff P S) H F FS
|
||||||
|
|
||||||
|
theorem eventually_sup_iff (P : A → Prop) (F₁ F₂ : filter A) :
|
||||||
|
eventually P (F₁ ⊔ F₂) ↔ eventually P F₁ ∧ eventually P F₂ :=
|
||||||
|
by rewrite [↑eventually, sets_sup]
|
||||||
|
|
||||||
|
theorem eventually_sup {P : A → Prop} {F₁ F₂ : filter A}
|
||||||
|
(H₁ : eventually P F₁) (H₂ : eventually P F₂) :
|
||||||
|
eventually P (F₁ ⊔ F₂) :=
|
||||||
|
iff.mpr (eventually_sup_iff P F₁ F₂) (and.intro H₁ H₂)
|
||||||
|
|
||||||
|
theorem eventually_of_eventually_sup_left {P : A → Prop} {F₁ F₂ : filter A}
|
||||||
|
(H : eventually P (F₁ ⊔ F₂)) : eventually P F₁ :=
|
||||||
|
and.left (iff.mp (eventually_sup_iff P F₁ F₂) H)
|
||||||
|
|
||||||
|
theorem eventually_of_eventually_sup_right {P : A → Prop} {F₁ F₂ : filter A}
|
||||||
|
(H : eventually P (F₁ ⊔ F₂)) : eventually P F₂ :=
|
||||||
|
and.right (iff.mp (eventually_sup_iff P F₁ F₂) H)
|
||||||
|
|
||||||
|
theorem eventually_inf_iff (P : A → Prop) (F₁ F₂ : filter A) :
|
||||||
|
eventually P (F₁ ⊓ F₂) ↔ (∃ S, eventually S F₁ ∧ ∃ T, eventually T F₂ ∧ (P ⊇ S ∩ T)) :=
|
||||||
|
by rewrite [↑eventually, sets_inf]
|
||||||
|
|
||||||
|
theorem eventually_inf {P : A → Prop} {F₁ F₂ : filter A}
|
||||||
|
{S : A → Prop} (HS : eventually S F₁) (T : A → Prop) (HT : eventually T F₂) (HP : P ⊇ S ∩ T) :
|
||||||
|
eventually P (F₁ ⊓ F₂) :=
|
||||||
|
iff.mpr (eventually_inf_iff P F₁ F₂)
|
||||||
|
(exists.intro S (and.intro HS (exists.intro T (and.intro HT HP))))
|
||||||
|
|
||||||
|
theorem exists_of_eventually_inf {P : A → Prop} {F₁ F₂ : filter A} (H : eventually P (F₁ ⊓ F₂)) :
|
||||||
|
∃ S, eventually S F₁ ∧ ∃ T, eventually T F₂ ∧ (P ⊇ S ∩ T) :=
|
||||||
|
iff.mp (eventually_inf_iff P F₁ F₂) H
|
||||||
|
|
||||||
|
/- top and bot -/
|
||||||
|
|
||||||
|
protected definition bot (A : Type) : filter A :=
|
||||||
⦃ filter,
|
⦃ filter,
|
||||||
sets := univ,
|
sets := univ,
|
||||||
univ_mem_sets := trivial,
|
univ_mem_sets := trivial,
|
||||||
inter_closed := λ a b Ha Hb, trivial,
|
inter_closed := λ a b Ha Hb, trivial,
|
||||||
is_mono := λ a b Ha Hsub, trivial
|
is_mono := λ a b Ha Hsub, trivial
|
||||||
⦄
|
⦄
|
||||||
notation `⊥` := bot
|
|
||||||
|
|
||||||
definition top : filter A :=
|
protected definition top (A : Type) : filter A :=
|
||||||
⦃ filter,
|
⦃ filter,
|
||||||
sets := '{univ},
|
sets := '{univ},
|
||||||
univ_mem_sets := !or.inl rfl,
|
univ_mem_sets := !or.inl rfl,
|
||||||
|
|
@ -135,171 +344,40 @@ definition top : filter A :=
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
⦄
|
⦄
|
||||||
notation `⊤` := top
|
|
||||||
|
|
||||||
definition sup (F₁ F₂ : filter A) : filter A :=
|
protected theorem bot_eq : ⊥ = filter.bot A :=
|
||||||
⦃ filter,
|
le.antisymm !bot_le
|
||||||
sets := F₁ ∩ F₂,
|
begin
|
||||||
univ_mem_sets := and.intro (filter.univ_mem_sets F₁) (filter.univ_mem_sets F₂),
|
apply le_of_forall_eventually,
|
||||||
inter_closed := abstract
|
intro P H,
|
||||||
λ a b Ha Hb,
|
apply mem_univ
|
||||||
and.intro
|
end
|
||||||
(filter.inter_closed F₁ (and.left Ha) (and.left Hb))
|
|
||||||
(filter.inter_closed F₂ (and.right Ha) (and.right Hb))
|
|
||||||
end,
|
|
||||||
is_mono := abstract
|
|
||||||
λ a b Hsub Ha,
|
|
||||||
and.intro
|
|
||||||
(filter.is_mono F₁ Hsub (and.left Ha))
|
|
||||||
(filter.is_mono F₂ Hsub (and.right Ha))
|
|
||||||
end
|
|
||||||
⦄
|
|
||||||
infix `⊔`:65 := sup
|
|
||||||
|
|
||||||
definition inf (F₁ F₂ : filter A) : filter A :=
|
protected theorem top_eq : ⊤ = filter.top A :=
|
||||||
⦃ filter,
|
le.antisymm
|
||||||
sets := {r | ∃₀ s ∈ F₁, ∃₀ t ∈ F₂, r ⊇ s ∩ t},
|
(le_of_forall_eventually
|
||||||
univ_mem_sets := abstract
|
(λ P H,
|
||||||
bounded_exists.intro (univ_mem_sets F₁)
|
have P = univ, from eq_of_mem_singleton H,
|
||||||
(bounded_exists.intro (univ_mem_sets F₂)
|
by+ rewrite this; apply eventually_true ⊤))
|
||||||
(by rewrite univ_inter; apply subset.refl))
|
!le_top
|
||||||
end,
|
|
||||||
inter_closed := abstract
|
|
||||||
λ a b Ha Hb,
|
|
||||||
obtain a₁ [a₁F₁ [a₂ [a₂F₂ (Ha' : a ⊇ a₁ ∩ a₂)]]], from Ha,
|
|
||||||
obtain b₁ [b₁F₁ [b₂ [b₂F₂ (Hb' : b ⊇ b₁ ∩ b₂)]]], from Hb,
|
|
||||||
assert a₁ ∩ b₁ ∩ (a₂ ∩ b₂) = a₁ ∩ a₂ ∩ (b₁ ∩ b₂),
|
|
||||||
by rewrite [*inter_assoc, inter_left_comm b₁],
|
|
||||||
have a ∩ b ⊇ a₁ ∩ b₁ ∩ (a₂ ∩ b₂),
|
|
||||||
begin
|
|
||||||
rewrite this,
|
|
||||||
apply subset_inter,
|
|
||||||
{apply subset.trans,
|
|
||||||
apply inter_subset_left,
|
|
||||||
exact Ha'},
|
|
||||||
apply subset.trans,
|
|
||||||
apply inter_subset_right,
|
|
||||||
exact Hb'
|
|
||||||
end,
|
|
||||||
bounded_exists.intro (inter_closed F₁ a₁F₁ b₁F₁)
|
|
||||||
(bounded_exists.intro (inter_closed F₂ a₂F₂ b₂F₂)
|
|
||||||
this)
|
|
||||||
end,
|
|
||||||
is_mono := abstract
|
|
||||||
λ a b Hsub Ha,
|
|
||||||
obtain a₁ [a₁F₁ [a₂ [a₂F₂ (Ha' : a ⊇ a₁ ∩ a₂)]]], from Ha,
|
|
||||||
bounded_exists.intro a₁F₁
|
|
||||||
(bounded_exists.intro a₂F₂ (subset.trans Ha' Hsub))
|
|
||||||
end
|
|
||||||
⦄
|
|
||||||
infix `⊓`:70 := inf
|
|
||||||
|
|
||||||
definition Sup (S : set (filter A)) : filter A :=
|
theorem sets_bot_eq : sets ⊥ = (univ : set (set A)) :=
|
||||||
⦃ filter,
|
by rewrite filter.bot_eq
|
||||||
sets := {s | ∀₀ F ∈ S, s ∈ F},
|
|
||||||
univ_mem_sets := λ F FS, univ_mem_sets F,
|
|
||||||
inter_closed := abstract
|
|
||||||
λ a b Ha Hb F FS,
|
|
||||||
inter_closed F (Ha F FS) (Hb F FS)
|
|
||||||
end,
|
|
||||||
is_mono := abstract
|
|
||||||
λ a b asubb Ha F FS,
|
|
||||||
is_mono F asubb (Ha F FS)
|
|
||||||
end
|
|
||||||
⦄
|
|
||||||
prefix `⨆`:65 := Sup
|
|
||||||
|
|
||||||
definition Inf (S : set (filter A)) : filter A :=
|
theorem sets_top_eq : sets ⊤ = ('{univ} : set (set A)) :=
|
||||||
Sup {F | ∀ G, G ∈ S → G ≽ F}
|
by rewrite filter.top_eq
|
||||||
|
|
||||||
prefix `⨅`:70 := Inf
|
theorem eventually_bot (P : A → Prop) : eventually P ⊥ :=
|
||||||
|
by rewrite [↑eventually, sets_bot_eq]; apply mem_univ
|
||||||
theorem eventually_of_refines (H₁ : eventually P F₁) (H₂ : F₁ ≽ F₂) : eventually P F₂ := H₂ H₁
|
|
||||||
|
|
||||||
theorem refines_of_forall (H : ∀ P, eventually P F₁ → eventually P F₂) : F₁ ≽ F₂ := H
|
|
||||||
|
|
||||||
theorem eventually_bot (P : A → Prop) : eventually P ⊥ := trivial
|
|
||||||
|
|
||||||
theorem refines_bot (F : filter A) : F ≽ ⊥ :=
|
|
||||||
take P, suppose eventually P F, eventually_bot P
|
|
||||||
|
|
||||||
theorem eventually_top_of_forall (H : ∀ x, P x) : eventually P ⊤ :=
|
theorem eventually_top_of_forall (H : ∀ x, P x) : eventually P ⊤ :=
|
||||||
by rewrite [↑eventually, ↑top, mem_singleton_iff]; exact eq_univ_of_forall H
|
by rewrite [↑eventually, sets_top_eq, mem_singleton_iff]; exact eq_univ_of_forall H
|
||||||
|
|
||||||
theorem forall_of_eventually_top : eventually P ⊤ → ∀ x, P x :=
|
theorem forall_of_eventually_top : eventually P ⊤ → ∀ x, P x :=
|
||||||
by rewrite [↑eventually, ↑top, mem_singleton_iff]; intro H x; rewrite H; exact trivial
|
by rewrite [↑eventually, sets_top_eq, mem_singleton_iff]; intro H x; rewrite H; exact trivial
|
||||||
|
|
||||||
theorem eventually_top (P : A → Prop) : eventually P top ↔ ∀ x, P x :=
|
theorem eventually_top_iff (P : A → Prop) : eventually P top ↔ ∀ x, P x :=
|
||||||
iff.intro forall_of_eventually_top eventually_top_of_forall
|
iff.intro forall_of_eventually_top eventually_top_of_forall
|
||||||
|
|
||||||
theorem top_refines (F : filter A) : ⊤ ≽ F :=
|
|
||||||
take P, suppose eventually P top,
|
|
||||||
eventually_of_forall F (forall_of_eventually_top this)
|
|
||||||
|
|
||||||
theorem eventually_sup (P : A → Prop) (F₁ F₂ : filter A) :
|
|
||||||
eventually P (sup F₁ F₂) ↔ eventually P F₁ ∧ eventually P F₂ :=
|
|
||||||
!iff.refl
|
|
||||||
|
|
||||||
theorem sup_refines_left (F₁ F₂ : filter A) : F₁ ⊔ F₂ ≽ F₁ :=
|
|
||||||
inter_subset_left _ _
|
|
||||||
|
|
||||||
theorem sup_refines_right (F₁ F₂ : filter A) : F₁ ⊔ F₂ ≽ F₂ :=
|
|
||||||
inter_subset_right _ _
|
|
||||||
|
|
||||||
theorem refines_sup (H₁ : F ≽ F₁) (H₂ : F ≽ F₂) : F ≽ F₁ ⊔ F₂ :=
|
|
||||||
subset_inter H₁ H₂
|
|
||||||
|
|
||||||
theorem refines_inf_left (F₁ F₂ : filter A) : F₁ ≽ F₁ ⊓ F₂ :=
|
|
||||||
take s, suppose s ∈ F₁,
|
|
||||||
bounded_exists.intro `s ∈ F₁`
|
|
||||||
(bounded_exists.intro (univ_mem_sets F₂) (by rewrite inter_univ; apply subset.refl))
|
|
||||||
|
|
||||||
theorem refines_inf_right (F₁ F₂ : filter A) : F₂ ≽ F₁ ⊓ F₂ :=
|
|
||||||
take s, suppose s ∈ F₂,
|
|
||||||
bounded_exists.intro (univ_mem_sets F₁)
|
|
||||||
(bounded_exists.intro `s ∈ F₂` (by rewrite univ_inter; apply subset.refl))
|
|
||||||
|
|
||||||
theorem inf_refines (H₁ : F₁ ≽ F) (H₂ : F₂ ≽ F) : F₁ ⊓ F₂ ≽ F :=
|
|
||||||
take s : set A, suppose (#set.filter s ∈ F₁ ⊓ F₂),
|
|
||||||
obtain a₁ [a₁F₁ [a₂ [a₂F₂ (Hsub : s ⊇ a₁ ∩ a₂)]]], from this,
|
|
||||||
have a₁ ∈ F, from H₁ a₁F₁,
|
|
||||||
have a₂ ∈ F, from H₂ a₂F₂,
|
|
||||||
show s ∈ F, from is_mono F Hsub (inter_closed F `a₁ ∈ F` `a₂ ∈ F`)
|
|
||||||
|
|
||||||
theorem refines_Sup {F : filter A} {S : set (filter A)} (H : ∀₀ G ∈ S, F ≽ G) : F ≽ ⨆ S :=
|
|
||||||
λ s Fs G GS, H GS Fs
|
|
||||||
|
|
||||||
theorem Sup_refines {F : filter A} {S : set (filter A)} (FS : F ∈ S) : ⨆ S ≽ F :=
|
|
||||||
λ s sInfS, sInfS F FS
|
|
||||||
|
|
||||||
theorem Inf_refines {F : filter A} {S : set (filter A)} (H : ∀₀ G ∈ S, G ≽ F) : ⨅ S ≽ F :=
|
|
||||||
Sup_refines H
|
|
||||||
|
|
||||||
theorem refines_Inf {F : filter A} {S : set (filter A)} (FS : F ∈ S) : F ≽ ⨅ S :=
|
|
||||||
refines_Sup (λ G GS, GS F FS)
|
|
||||||
|
|
||||||
protected definition complete_lattice_Inf [reducible] [instance] : complete_lattice_Inf (filter A) :=
|
|
||||||
⦃ complete_lattice_Inf,
|
|
||||||
le := weakens,
|
|
||||||
le_refl := weakens.refl,
|
|
||||||
le_trans := @weakens.trans A,
|
|
||||||
le_antisymm := @weakens.antisymm A,
|
|
||||||
-- inf := inf,
|
|
||||||
-- le_inf := @inf_refines A,
|
|
||||||
-- inf_le_left := refines_inf_left,
|
|
||||||
-- inf_le_right := refines_inf_right,
|
|
||||||
-- sup := sup,
|
|
||||||
-- sup_le := @refines_sup A,
|
|
||||||
-- le_sup_left := sup_refines_left,
|
|
||||||
-- le_sup_right := sup_refines_right,
|
|
||||||
Inf := Inf,
|
|
||||||
Inf_le := @refines_Inf A,
|
|
||||||
le_Inf := @Inf_refines A
|
|
||||||
⦄
|
|
||||||
|
|
||||||
-- The previous instance is enough for showing that (filter A) is a complete_lattice
|
|
||||||
example {A : Type} : complete_lattice (filter A) :=
|
|
||||||
_
|
|
||||||
|
|
||||||
end filter
|
end filter
|
||||||
end set
|
end set
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue