Indicator function and filters
Properties of indicator functions involving =ᶠ and ≤ᶠ.
Tags
indicator, characteristic, filter
theorem
tendsto_indicator_of_monotone
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[preorder ι]
[has_zero β]
(s : ι → set α)
(hs : monotone s)
(f : α → β)
(a : α) :
filter.tendsto (λ (i : ι), (s i).indicator f a) filter.at_top (has_pure.pure ((⋃ (i : ι), s i).indicator f a))
theorem
tendsto_indicator_of_antimono
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[preorder ι]
[has_zero β]
(s : ι → set α)
(hs : ∀ ⦃i j : ι⦄, i ≤ j → s j ⊆ s i)
(f : α → β)
(a : α) :
filter.tendsto (λ (i : ι), (s i).indicator f a) filter.at_top (has_pure.pure ((⋂ (i : ι), s i).indicator f a))
theorem
tendsto_indicator_bUnion_finset
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[has_zero β]
(s : ι → set α)
(f : α → β)
(a : α) :
filter.tendsto (λ (n : finset ι), (⋃ (i : ι) (H : i ∈ n), s i).indicator f a) filter.at_top (has_pure.pure ((set.Union s).indicator f a))