Filters with a cardinal intersection property

In this file we define CardinalInterFilter l c to be the class of filters with the following property: for any collection of sets s ∈ l with cardinality strictly less than c, their intersection belongs to l as well.

Main results

• Filter.cardinalInterFilter_aleph0 establishes that every filter l is a CardinalInterFilter l ℵ₀
• CardinalInterFilter.toCountableInterFilter establishes that every CardinalInterFilter l c with c > ℵ₀ is a CountableInterFilter.
• CountableInterFilter.toCardinalInterFilter establishes that every CountableInterFilter l is a CardinalInterFilter l ℵ₁.
• CardinalInterFilter.of_CardinalInterFilter_of_lt establishes that we have CardinalInterFilter l c → CardinalInterFilter l a for all a < c.

Tags

filter, cardinal

class CardinalInterFilter {α : Type u} (l : Filter α) (c : Cardinal.{u}) : Prop

A filter l has the cardinal c intersection property if for any collection of less than c sets s ∈ l, their intersection belongs to l as well.

• cardinal_sInter_mem (S : Set (Set α)) : Cardinal.mk ↑S < c → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l

  For a collection of sets s ∈ l with cardinality below c, their intersection belongs to l as well.

theorem cardinal_sInter_mem {α : Type u} {c : Cardinal.{u}} {l : Filter α} {S : Set (Set α)} [CardinalInterFilter l c] (hSc : Cardinal.mk ↑S < c) : ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l

theorem Filter.cardinalInterFilter_aleph0 {α : Type u} (l : Filter α) : CardinalInterFilter l Cardinal.aleph0

Every filter is a CardinalInterFilter with c = ℵ₀

theorem CardinalInterFilter.toCountableInterFilter {α : Type u} {c : Cardinal.{u}} (l : Filter α) [CardinalInterFilter l c] (hc : Cardinal.aleph0 < c) : CountableInterFilter l

Every CardinalInterFilter with c > ℵ₀ is a CountableInterFilter

instance CountableInterFilter.toCardinalInterFilter {α : Type u} (l : Filter α) [CountableInterFilter l] : CardinalInterFilter l (Cardinal.aleph 1)

Every CountableInterFilter is a CardinalInterFilter with c = ℵ₁

theorem cardinalInterFilter_aleph_one_iff {α : Type u} {l : Filter α} : CardinalInterFilter l (Cardinal.aleph 1) ↔ CountableInterFilter l

theorem CardinalInterFilter.of_cardinalInterFilter_of_le {α : Type u} {c : Cardinal.{u}} (l : Filter α) [CardinalInterFilter l c] {a : Cardinal.{u}} (hac : a ≤ c) : CardinalInterFilter l a

Every CardinalInterFilter for some c also is a CardinalInterFilter for some a ≤ c

theorem CardinalInterFilter.of_cardinalInterFilter_of_lt {α : Type u} {c : Cardinal.{u}} (l : Filter α) [CardinalInterFilter l c] {a : Cardinal.{u}} (hac : a < c) : CardinalInterFilter l a

theorem Filter.cardinal_iInter_mem {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s : ι → Set α} (hic : Cardinal.mk ι < c) : ⋂ (i : ι), s i ∈ l ↔ ∀ (i : ι), s i ∈ l

theorem Filter.cardinal_bInter_mem {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk ↑S < c) {s : (i : ι) → i ∈ S → Set α} : ⋂ (i : ι), ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

theorem Filter.eventually_cardinal_forall {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {p : α → ι → Prop} (hic : Cardinal.mk ι < c) : (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

theorem Filter.eventually_cardinal_ball {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk ↑S < c) {p : α → (i : ι) → i ∈ S → Prop} : (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

theorem Filter.EventuallyLE.cardinal_iUnion {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s t : ι → Set α} (hic : Cardinal.mk ι < c) (h : ∀ (i : ι), s i ≤ᶠ[l] t i) : ⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i

theorem Filter.EventuallyEq.cardinal_iUnion {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s t : ι → Set α} (hic : Cardinal.mk ι < c) (h : ∀ (i : ι), s i =ᶠ[l] t i) : ⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i

theorem Filter.EventuallyLE.cardinal_bUnion {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk ↑S < c) {s t : (i : ι) → i ∈ S → Set α} (h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) : ⋃ (i : ι), ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ (i : ι), ⋃ (h : i ∈ S), t i h

theorem Filter.EventuallyEq.cardinal_bUnion {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk ↑S < c) {s t : (i : ι) → i ∈ S → Set α} (h : ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) : ⋃ (i : ι), ⋃ (h : i ∈ S), s i h =ᶠ[l] ⋃ (i : ι), ⋃ (h : i ∈ S), t i h

theorem Filter.EventuallyLE.cardinal_iInter {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s t : ι → Set α} (hic : Cardinal.mk ι < c) (h : ∀ (i : ι), s i ≤ᶠ[l] t i) : ⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i

theorem Filter.EventuallyEq.cardinal_iInter {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s t : ι → Set α} (hic : Cardinal.mk ι < c) (h : ∀ (i : ι), s i =ᶠ[l] t i) : ⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i

theorem Filter.EventuallyLE.cardinal_bInter {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk ↑S < c) {s t : (i : ι) → i ∈ S → Set α} (h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) : ⋂ (i : ι), ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ (i : ι), ⋂ (h : i ∈ S), t i h

theorem Filter.EventuallyEq.cardinal_bInter {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk ↑S < c) {s t : (i : ι) → i ∈ S → Set α} (h : ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) : ⋂ (i : ι), ⋂ (h : i ∈ S), s i h =ᶠ[l] ⋂ (i : ι), ⋂ (h : i ∈ S), t i h

def Filter.ofCardinalInter {α : Type u} {c : Cardinal.{u}} (l : Set (Set α)) (hc : 2 < c) (hl : ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) : Filter α

Construct a filter with cardinal c intersection property. This constructor deduces Filter.univ_sets and Filter.inter_sets from the cardinal c intersection property.

Equations

• Filter.ofCardinalInter l hc hl h_mono = { sets := l, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

instance Filter.cardinalInter_ofCardinalInter {α : Type u} {c : Cardinal.{u}} (l : Set (Set α)) (hc : 2 < c) (hl : ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) : CardinalInterFilter (ofCardinalInter l hc hl h_mono) c

@[simp]

theorem Filter.mem_ofCardinalInter {α : Type u} {c : Cardinal.{u}} {l : Set (Set α)} (hc : 2 < c) (hl : ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) {s : Set α} : s ∈ ofCardinalInter l hc hl h_mono ↔ s ∈ l

def Filter.ofCardinalUnion {α : Type u} {c : Cardinal.{u}} (l : Set (Set α)) (hc : 2 < c) (hUnion : ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) (hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) : Filter α

Construct a filter with cardinal c intersection property. Similarly to Filter.comk, a set belongs to this filter if its complement satisfies the property. Similarly to Filter.ofCardinalInter, this constructor deduces some properties from the cardinal c intersection property which becomes the cardinal c union property because we take complements of all sets.

Equations

• Filter.ofCardinalUnion l hc hUnion hmono = Filter.ofCardinalInter {s : Set α | sᶜ ∈ l} hc ⋯ ⋯

instance Filter.cardinalInter_ofCardinalUnion {α : Type u} {c : Cardinal.{u}} (l : Set (Set α)) (hc : 2 < c) (h₁ : ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) (h₂ : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) : CardinalInterFilter (ofCardinalUnion l hc h₁ h₂) c

@[simp]

theorem Filter.mem_ofCardinalUnion {α : Type u} {c : Cardinal.{u}} {l : Set (Set α)} (hc : 2 < c) {hunion : ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l} {hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l} {s : Set α} : s ∈ ofCardinalUnion l hc hunion hmono ↔ l sᶜ

instance Filter.cardinalInterFilter_principal {α : Type u} {c : Cardinal.{u}} (s : Set α) : CardinalInterFilter (principal s) c

instance Filter.cardinalInterFilter_bot {α : Type u} {c : Cardinal.{u}} : CardinalInterFilter ⊥ c

instance Filter.cardinalInterFilter_top {α : Type u} {c : Cardinal.{u}} : CardinalInterFilter ⊤ c

instance Filter.instCardinalInterFilterComap {α β : Type u} {c : Cardinal.{u}} (l : Filter β) [CardinalInterFilter l c] (f : α → β) : CardinalInterFilter (comap f l) c

instance Filter.instCardinalInterFilterMap {α β : Type u} {c : Cardinal.{u}} (l : Filter α) [CardinalInterFilter l c] (f : α → β) : CardinalInterFilter (map f l) c

instance Filter.cardinalInterFilter_inf_eq {α : Type u} {c : Cardinal.{u}} (l₁ l₂ : Filter α) [CardinalInterFilter l₁ c] [CardinalInterFilter l₂ c] : CardinalInterFilter (l₁ ⊓ l₂) c

Infimum of two CardinalInterFilters is a CardinalInterFilter. This is useful, e.g., to automatically get an instance for residual α ⊓ 𝓟 s.

instance Filter.cardinalInterFilter_inf {α : Type u} (l₁ l₂ : Filter α) {c₁ c₂ : Cardinal.{u}} [CardinalInterFilter l₁ c₁] [CardinalInterFilter l₂ c₂] : CardinalInterFilter (l₁ ⊓ l₂) (min c₁ c₂)

instance Filter.cardinalInterFilter_sup_eq {α : Type u} {c : Cardinal.{u}} (l₁ l₂ : Filter α) [CardinalInterFilter l₁ c] [CardinalInterFilter l₂ c] : CardinalInterFilter (l₁ ⊔ l₂) c

Supremum of two CardinalInterFilters is a CardinalInterFilter.

instance Filter.cardinalInterFilter_sup {α : Type u} (l₁ l₂ : Filter α) {c₁ c₂ : Cardinal.{u}} [CardinalInterFilter l₁ c₁] [CardinalInterFilter l₂ c₂] : CardinalInterFilter (l₁ ⊔ l₂) (min c₁ c₂)

inductive Filter.CardinalGenerateSets {α : Type u} {c : Cardinal.{u}} (g : Set (Set α)) : Set α → Prop

Filter.CardinalGenerateSets c g is the (sets of the) greatest cardinalInterFilter c containing g.

• basic {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {s : Set α} : s ∈ g → CardinalGenerateSets g s
• univ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} : CardinalGenerateSets g Set.univ
• superset {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {s t : Set α} : CardinalGenerateSets g s → s ⊆ t → CardinalGenerateSets g t
• sInter {α : Type u} {c : Cardinal.{u}} {g S : Set (Set α)} : Cardinal.mk ↑S < c → (∀ s ∈ S, CardinalGenerateSets g s) → CardinalGenerateSets g (⋂₀ S)

def Filter.cardinalGenerate {α : Type u} {c : Cardinal.{u}} (g : Set (Set α)) (hc : 2 < c) : Filter α

Filter.cardinalGenerate c g is the greatest cardinalInterFilter c containing g.

Equations

• Filter.cardinalGenerate g hc = Filter.ofCardinalInter (Filter.CardinalGenerateSets g) hc ⋯ ⋯

theorem Filter.cardinalInter_ofCardinalGenerate {α : Type u} {c : Cardinal.{u}} (g : Set (Set α)) (hc : 2 < c) : CardinalInterFilter (cardinalGenerate g hc) c

theorem Filter.mem_cardinaleGenerate_iff {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {s : Set α} {hreg : c.IsRegular} : s ∈ cardinalGenerate g ⋯ ↔ ∃ S ⊆ g, Cardinal.mk ↑S < c ∧ ⋂₀ S ⊆ s

A set is in the cardinalInterFilter generated by g if and only if it contains an intersection of c elements of g.

theorem Filter.le_cardinalGenerate_iff_of_cardinalInterFilter {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {f : Filter α} [CardinalInterFilter f c] (hc : 2 < c) : f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets

theorem Filter.cardinalGenerate_isGreatest {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} (hc : 2 < c) : IsGreatest {f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets} (cardinalGenerate g hc)

cardinalGenerate g hc is the greatest cardinalInterFilter c containing g.