mathlib documentation

order.filter.indicator_function

Indicator function and filters #

Properties of indicator functions involving =ᶠ and ≤ᶠ.

Tags #

indicator, characteristic, filter

theorem indicator_eventually_eq {α : Type u_1} {M : Type u_3} [has_zero M] {s t : set α} {f g : α → M} {l : filter α} (hf : f =ᶠ[l 𝓟 s] g) (hs : s =ᶠ[l] t) :
theorem indicator_union_eventually_eq {α : Type u_1} {M : Type u_3} [add_monoid M] {s t : set α} {f : α → M} {l : filter α} (h : ∀ᶠ (a : α) in l, a s t) :
theorem indicator_eventually_le_indicator {α : Type u_1} {β : Type u_2} [has_zero β] [preorder β] {s : set α} {f g : α → β} {l : filter α} (h : f ≤ᶠ[l 𝓟 s] g) :
theorem monotone.tendsto_indicator {α : 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 (pure ((⋃ (i : ι), s i).indicator f a))
theorem antitone.tendsto_indicator {α : Type u_1} {β : Type u_2} {ι : Type u_3} [preorder ι] [has_zero β] (s : ι → set α) (hs : antitone s) (f : α → β) (a : α) :
filter.tendsto (λ (i : ι), (s i).indicator f a) filter.at_top (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 (pure ((set.Union s).indicator f a))