Filters with countable intersection property
In this file we define countable_Inter_filter to be the class of filters with the following
property: for any countable collection of sets s ∈ l their intersection belongs to l as well.
Two main examples are the residual filter defined in topology.metric_space.baire and
the measure.ae filter defined in measure_theory.measure_space.
theorem
countable_Inter_mem_sets
{ι : Type u_1}
{α : Type u_2}
{l : filter α}
[countable_Inter_filter l]
[encodable ι]
{s : ι → set α} :
theorem
eventually_countable_forall
{ι : Type u_1}
{α : Type u_2}
{l : filter α}
[countable_Inter_filter l]
[encodable ι]
{p : α → ι → Prop} :
(∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
theorem
eventually_countable_ball
{ι : Type u_1}
{α : Type u_2}
{l : filter α}
[countable_Inter_filter l]
{S : set ι}
(hS : S.countable)
{p : α → Π (i : ι), i ∈ S → Prop} :
@[instance]
Equations
@[instance]
Equations
@[instance]
def
countable_Inter_filter_inf
{α : Type u_2}
(l₁ l₂ : filter α)
[countable_Inter_filter l₁]
[countable_Inter_filter l₂] :
countable_Inter_filter (l₁ ⊓ l₂)
Infimum of two countable_Inter_filters is a countable_Inter_filter. This is useful, e.g.,
to automatically get an instance for residual α ⊓ 𝓟 s.
Equations
- _ = _
@[instance]
def
countable_Inter_filter_sup
{α : Type u_2}
(l₁ l₂ : filter α)
[countable_Inter_filter l₁]
[countable_Inter_filter l₂] :
countable_Inter_filter (l₁ ⊔ l₂)
Supremum of two countable_Inter_filters is a countable_Inter_filter.
Equations
- _ = _