Indicator function and filters #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ⊓ filter.principal 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 ⊓ filter.principal 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 : α) :

theorem antitone.tendsto_indicator {α : Type u_1} {β : Type u_2} {ι : Type u_3} [preorder ι] [has_zero β] (s : ι → set α) (hs : antitone s) (f : α → β) (a : α) :

theorem tendsto_indicator_bUnion_finset {α : Type u_1} {β : Type u_2} {ι : Type u_3} [has_zero β] (s : ι → set α) (f : α → β) (a : α) :

theorem filter.eventually_eq.support {α : Type u_1} {β : Type u_2} [has_zero β] {f g : α → β} {l : filter α} (h : f =ᶠ[l] g) :

theorem filter.eventually_eq.indicator {α : Type u_1} {β : Type u_2} [has_zero β] {l : filter α} {f g : α → β} {s : set α} (hfg : f =ᶠ[l] g) :

theorem filter.eventually_eq.indicator_zero {α : Type u_1} {β : Type u_2} [has_zero β] {l : filter α} {f : α → β} {s : set α} (hf : f =ᶠ[l] 0) :