feat(library/data/set/filter): work in material from Jacob Gross

library/data/set/filter.lean

@@ -34,12 +34,16 @@ P ∈ F
 theorem eventually_true (F : filter A) : eventually (λx, true) F :=
 !filter.univ_mem_sets
 
-theorem eventually_of_forall {P : A → Prop} (F : filter A) (H : ∀ x, P x) : eventually P F :=
+theorem eventually_of_forall (F : filter A) (H : ∀ x, P x) : eventually P F :=
 by rewrite [eq_univ_of_forall H]; apply eventually_true
 
 theorem eventually_mono (H₁ : eventually P F) (H₂ : ∀x, P x → Q x) : eventually Q F :=
 !filter.is_mono H₂ H₁
 
+theorem eventually_congr (H : ∀ x, P x ↔ Q x) (H' : eventually P F) : eventually Q F :=
+have P = Q, from ext H,
+using this, by rewrite -this; exact H'
+
 theorem eventually_and (H₁ : eventually P F) (H₂ : eventually Q F) :
   eventually (λ x, P x ∧ Q x) F :=
 !filter.inter_closed H₁ H₂
@@ -95,6 +99,54 @@ 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 :=
 iff.intro (eventually_iff_mp H) (eventually_iff_mpr H)
 
+/- frequently -/
+
+definition frequently (P : A → Prop) (F : filter A) : Prop := ¬ eventually (λ x, ¬ P x) F
+
+theorem not_frequently_of_eventually : eventually (λ x, ¬ P x) F → ¬ frequently P F :=
+not_not_intro
+
+theorem frequently_mono (H₁ : frequently P F) (H₂ : ∀ x, P x → Q x) : frequently Q F :=
+ not.mto (λ H, eventually_mono H ( λ x, not.mto (H₂ x)))  H₁
+
+theorem frequently_mp (ev : eventually (λ x, P x → Q x) F) :
+  frequently P F → frequently Q F :=
+not.mto (λ H, eventually_mp (eventually_mono ev (λ x HPQ, not.mto HPQ)) H)
+
+theorem not_frequently_false : ¬ frequently (λ x, false) F :=
+begin
+  apply not_not_intro,
+  apply eventually_congr,
+  intro x, apply iff.symm not_false_iff,
+  exact eventually_true F
+end
+
+section
+  open classical
+
+  theorem not_frequently_iff  : ¬ frequently P F ↔ eventually (λ x, ¬ P x) F :=
+  by unfold frequently; rewrite not_not_iff
+
+  theorem exists_of_frequently : frequently P F → ∃ x, P x :=
+  assume H, obtain x Hx, from !exists_not_of_not_eventually H,
+  show _, from exists.intro x (not_not_elim Hx)
+
+  theorem frequently_inl (H : frequently P F) : frequently (λx, P x ∨ Q x) F :=
+  assume H' : eventually (λx, ¬ (P x ∨ Q x)) F,
+  have (λx, ¬ (P x ∨ Q x)) = λ x, ¬ P x ∧ ¬ Q x,
+    by apply funext; intro x; rewrite not_or_iff_not_and_not,
+  show false, using this,
+    by rewrite this at H'; exact H (eventually_of_eventually_and_left H')
+
+  theorem frequently_inr (H : frequently Q F) : frequently (λx, P x ∨ Q x) F :=
+  begin
+    apply frequently_mp,
+    apply eventually_of_forall,
+    intro x, apply or.swap,
+    exact frequently_inl H
+  end
+end
+
 /- filters form a lattice under ⊇ -/
 
 protected theorem eq : sets F₁ = sets F₂ → F₁ = F₂ :=
@@ -257,9 +309,9 @@ protected definition complete_lattice [reducible] [trans_instance] : complete_la
   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 : F₁ ≤ F₂) : sets F₂ ⊆ sets F₁ := H
 
-protected theorem subset_of_le {F₁ F₂ : filter A} (H : sets F₂ ⊆ sets F₁) : F₁ ≤ F₂ := H
+protected theorem le_of_subset {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
 
@@ -379,5 +431,128 @@ by rewrite [↑eventually, sets_top_eq, mem_singleton_iff]; intro H x; rewrite H
 theorem eventually_top_iff (P : A → Prop) : eventually P top ↔ ∀ x, P x :=
 iff.intro forall_of_eventually_top eventually_top_of_forall
 
+/- filter generated by a collection of sets -/
+
+inductive sets_generated_by {A : Type} (B : set (set A)) : set A → Prop :=
+| generators_mem : ∀ ⦃s : set A⦄, s ∈ B → sets_generated_by B s
+| univ_mem : sets_generated_by B univ
+| inter_mem : ∀ {a b}, sets_generated_by B a → sets_generated_by B b → sets_generated_by B (a ∩ b)
+| mono : ∀ {a b}, a ⊆ b → sets_generated_by B a → sets_generated_by B b
+
+definition filter_generated_by [reducible] {A : Type} (B : set (set A)) : filter A :=
+⦃filter,
+  sets            := sets_generated_by B,
+  univ_mem_sets   := sets_generated_by.univ_mem B,
+  inter_closed    := @sets_generated_by.inter_mem A B,
+  is_mono         := @sets_generated_by.mono A B ⦄
+
+theorem generators_subset_generated_by (B : set (set A)) : B ⊆ filter_generated_by B :=
+λ s H, sets_generated_by.generators_mem H
+
+theorem sets_generated_by_initial {B : set (set A)} {F : filter A} (H : B ⊆ sets F) :
+  sets_generated_by B ⊆ F :=
+begin
+  intro s Hs,
+  induction Hs with s sB s t os ot soA toA S SB SOA,
+    {exact H sB},
+    {exact filter.univ_mem_sets F},
+    {exact filter.inter_closed F soA toA},
+   exact filter.is_mono F SOA v_0
+end
+
+theorem le_filter_generated_by {B : set (set A)} {F : filter A}
+    (H : B ⊆ sets F) : F ≤ filter_generated_by B :=
+sets_generated_by_initial H
+
+/- principal filter -/
+
+definition principal (s : set A) : filter A := filter_generated_by '{s}
+
+theorem mem_principal (s : set A) : s ∈ principal s :=
+!generators_subset_generated_by !mem_singleton
+
+theorem eventually_principal {s : set A} {P : A → Prop} (H : s ⊆ P) : eventually P (principal s) :=
+!filter.is_mono H !mem_principal
+
+theorem subset_of_eventually_principal {s : set A} {P : A → Prop}
+  (H : eventually P (principal s)) : s ⊆ P :=
+begin
+  induction H with s' Ps' a b Ha Hb ssuba ssubb a b asubb Ha ssuba,
+    {rewrite [eq_of_mem_singleton Ps']; exact subset.refl s},
+    {exact subset_univ s},
+    {exact subset_inter ssuba ssubb},
+    {exact subset.trans ssuba asubb}
+end
+
+theorem eventually_principal_iff (s P : set A) : eventually P (principal s) ↔ (s ⊆ P) :=
+iff.intro subset_of_eventually_principal eventually_principal
+
+theorem sets_principal (s : set A) : sets (principal s) = { t | s ⊆ t } :=
+ext (take P, eventually_principal_iff s P)
+
+theorem principal_empty : principal (∅ : set A) = ⊥ :=
+begin
+  apply filter.eq,
+  rewrite [sets_principal, sets_bot_eq],
+  show { t | ∅ ⊆ t} = univ, from ext (take x, iff.intro
+    (assume H, trivial)
+    (assume H, empty_subset x))
+end
+
+theorem principal_univ_eq : principal (@univ A) = ⊤ :=
+begin
+  apply filter.eq,
+  rewrite [sets_principal, sets_top_eq],
+  show { t | univ ⊆ t} = '{univ}, from ext (take x, iff.intro
+    (assume H : univ ⊆ x, mem_singleton_of_eq (!eq_univ_of_univ_subset H))
+    (assume H : x ∈ '{univ}, by rewrite [eq_of_mem_singleton H]; apply subset.refl))
+end
+
+theorem principal_le_principal {s t : set A} (H : s ⊆ t) : principal s ≤ principal t :=
+begin
+  apply filter.le_of_subset,
+  rewrite *sets_principal,
+  show { u | t ⊆ u } ⊆ { u | s ⊆ u }, from
+    take u, suppose t ⊆ u, subset.trans H this
+end
+
+theorem subset_of_principal_le_principal {s t : set A} (H : principal s ≤ principal t) : s ⊆ t :=
+begin
+  note H' := filter.subset_of_le H,
+  revert H', rewrite *sets_principal,
+  intro H',
+  exact H' (subset.refl t)
+end
+
+theorem principal_refines_principal_iff {s t : set A} : principal s ≤ principal t ↔ s ⊆ t :=
+iff.intro subset_of_principal_le_principal principal_le_principal
+
+theorem principal_sup_principal {s t : set A} : principal s ⊔ principal t = principal (s ∪ t) :=
+begin
+  apply filter.eq,
+  rewrite [sets_sup, *sets_principal],
+  apply ext, intro u, apply iff.intro,
+    exact (suppose s ⊆ u ∧ t ⊆ u,
+      show s ∪ t ⊆ u, from union_subset (and.left this) (and.right this)),
+  exact suppose s ∪ t ⊆ u,
+    and.intro (subset.trans (subset_union_left _ _) this)
+              (subset.trans (subset_union_right _ _) this)
+end
+
+
+theorem principal_inf_principal {s t : set A} : principal s ⊓ principal t = principal (s ∩ t) :=
+begin
+  apply filter.eq,
+  rewrite [sets_inf, *sets_principal],
+  apply ext, intro u, apply iff.intro,
+    {intro H,
+      show s ∩ t ⊆ u, from
+        obtain s' [(ss' : s ⊆ s') [t' [(tt' : t ⊆ t') (Hu : s' ∩ t' ⊆ u)]]], from H,
+        take x, assume H', Hu (and.intro (ss' (and.left H')) (tt' (and.right H')))},
+  {intro H',
+    exact exists.intro s (and.intro (subset.refl s) (exists.intro t
+           (and.intro (subset.refl t) H')))}
+end
+
 end filter
 end set