Functions that are eventually constant along a filter

In this file we define a predicate Filter.EventuallyConst f l saying that a function f : α → β is eventually equal to a constant along a filter l. We also prove some basic properties of these functions.

We also define Filter.EventuallyEmptyOrUniv s l, the specialization of EventuallyConst to a set s : Set α, saying that s is eventually empty or eventually equal to univ along l.

Implementation notes

A naive definition of Filter.EventuallyConst f l is ∃ y, ∀ᶠ x in l, f x = y. However, this proposition is false for empty α, β. Instead, we say that Filter.map f l is supported on a subsingleton. This allows us to drop [Nonempty _] assumptions here and there.

def Filter.EventuallyConst {α : Type u_1} {β : Type u_2} (f : α → β) (l : Filter α) : Prop

The proposition that a function is eventually constant along a filter on the domain.

theorem Filter.HasBasis.eventuallyConst_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) : EventuallyConst f l ↔ ∃ (i : ι), p i ∧ ∀ x ∈ s i, ∀ y ∈ s i, f x = f y

theorem Filter.HasBasis.eventuallyConst_iff' {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α} {x : ι → α} (h : l.HasBasis p s) (hx : ∀ (i : ι), p i → x i ∈ s i) : EventuallyConst f l ↔ ∃ (i : ι), p i ∧ ∀ y ∈ s i, f y = f (x i)

theorem Filter.eventuallyConst_iff_tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Nonempty β] : EventuallyConst f l ↔ ∃ (x : β), Tendsto f l (pure x)

theorem Filter.EventuallyConst.exists_tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Nonempty β] : EventuallyConst f l → ∃ (x : β), Tendsto f l (pure x)

Alias of the forward direction of Filter.eventuallyConst_iff_tendsto.

theorem Filter.EventuallyConst.of_tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {x : β} (h : Tendsto f l (pure x)) : EventuallyConst f l

theorem Filter.eventuallyConst_iff_exists_eventuallyEq {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Nonempty β] : EventuallyConst f l ↔ ∃ (c : β), f =ᶠ[l] fun (x : α) => c

theorem Filter.EventuallyConst.eventuallyEq_const {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Nonempty β] : EventuallyConst f l → ∃ (c : β), f =ᶠ[l] fun (x : α) => c

Alias of the forward direction of Filter.eventuallyConst_iff_exists_eventuallyEq.

theorem Filter.eventuallyConst_pred' {α : Type u_1} {l : Filter α} {p : α → Prop} : EventuallyConst p l ↔ (p =ᶠ[l] fun (x : α) => False) ∨ p =ᶠ[l] fun (x : α) => True

theorem Filter.eventuallyConst_pred {α : Type u_1} {l : Filter α} {p : α → Prop} : EventuallyConst p l ↔ (∀ᶠ (x : α) in l, p x) ∨ ∀ᶠ (x : α) in l, ¬p x

def Filter.EventuallyEmptyOrUniv {α : Type u_1} (s : Set α) (l : Filter α) : Prop

A set s is eventually empty or eventually universal along a filter l if it is eventually equal to ∅ or to univ.

This is the specialization of Filter.EventuallyConst to s : Set α.

theorem Filter.eventuallyEmptyOrUniv_iff' {α : Type u_1} {l : Filter α} {s : Set α} : EventuallyEmptyOrUniv s l ↔ s =ᶠ[l] ∅ ∨ s =ᶠ[l] Set.univ

@[deprecated Filter.eventuallyEmptyOrUniv_iff' (since := "2026-08-25")]

theorem Filter.eventuallyConst_set' {α : Type u_1} {l : Filter α} {s : Set α} : EventuallyConst s l ↔ s =ᶠ[l] ∅ ∨ s =ᶠ[l] Set.univ

theorem Filter.eventuallyEmptyOrUniv_iff {α : Type u_1} {l : Filter α} {s : Set α} : EventuallyEmptyOrUniv s l ↔ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, x ∉ s

@[deprecated Filter.eventuallyEmptyOrUniv_iff (since := "2026-08-25")]

theorem Filter.eventuallyConst_set {α : Type u_1} {l : Filter α} {s : Set α} : EventuallyConst s l ↔ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, x ∉ s

theorem Filter.eventuallyEmptyOrUniv_preimage {α : Type u_1} {β : Type u_2} {l : Filter α} {s : Set β} {f : α → β} : EventuallyEmptyOrUniv (f ⁻¹' s) l ↔ EventuallyEmptyOrUniv s (map f l)

@[deprecated Filter.eventuallyEmptyOrUniv_preimage (since := "2026-08-25")]

theorem Filter.eventuallyConst_preimage {α : Type u_1} {β : Type u_2} {l : Filter α} {s : Set β} {f : α → β} : EventuallyConst (f ⁻¹' s) l ↔ EventuallyConst s (map f l)

theorem Filter.EventuallyEq.eventuallyConst_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) : EventuallyConst f l ↔ EventuallyConst g l

@[simp]

theorem Filter.eventuallyConst_id {α : Type u_1} {l : Filter α} : EventuallyConst id l ↔ l.Subsingleton

@[simp]

theorem Filter.EventuallyConst.bot {α : Type u_1} {β : Type u_2} {f : α → β} : EventuallyConst f ⊥

@[simp]

theorem Filter.EventuallyConst.const {α : Type u_1} {β : Type u_2} {l : Filter α} (c : β) : EventuallyConst (fun (x : α) => c) l

theorem Filter.EventuallyConst.congr {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β} (h : EventuallyConst f l) (hg : f =ᶠ[l] g) : EventuallyConst g l

theorem Filter.EventuallyConst.of_subsingleton_right {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Subsingleton β] : EventuallyConst f l

theorem Filter.EventuallyConst.anti {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {l' : Filter α} (h : EventuallyConst f l) (hl' : l' ≤ l) : EventuallyConst f l'

theorem Filter.EventuallyConst.of_subsingleton_left {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Subsingleton α] : EventuallyConst f l

theorem Filter.EventuallyConst.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β} (h : EventuallyConst f l) (g : β → γ) : EventuallyConst (g ∘ f) l

theorem Filter.EventuallyConst.inv {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Inv β] (h : EventuallyConst f l) : EventuallyConst f⁻¹ l

theorem Filter.EventuallyConst.neg {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Neg β] (h : EventuallyConst f l) : EventuallyConst (-f) l

theorem Filter.EventuallyConst.comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β} {lb : Filter β} {g : β → γ} (hg : EventuallyConst g lb) (hf : Tendsto f l lb) : EventuallyConst (g ∘ f) l

theorem Filter.EventuallyConst.apply {α : Type u_1} {l : Filter α} {ι : Type u_5} {p : ι → Type u_6} {g : α → (x : ι) → p x} (h : EventuallyConst g l) (i : ι) : EventuallyConst (fun (x : α) => g x i) l

theorem Filter.EventuallyConst.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} {f : α → β} {g : α → γ} (hf : EventuallyConst f l) (op : β → γ → δ) (hg : EventuallyConst g l) : EventuallyConst (fun (x : α) => op (f x) (g x)) l

theorem Filter.EventuallyConst.prodMk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β} {g : α → γ} (hf : EventuallyConst f l) (hg : EventuallyConst g l) : EventuallyConst (fun (x : α) => (f x, g x)) l

theorem Filter.EventuallyConst.mul {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Mul β] {g : α → β} (hf : EventuallyConst f l) (hg : EventuallyConst g l) : EventuallyConst (f * g) l

theorem Filter.EventuallyConst.add {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Add β] {g : α → β} (hf : EventuallyConst f l) (hg : EventuallyConst g l) : EventuallyConst (f + g) l

@[simp]

theorem Filter.EventuallyEmptyOrUniv.bot {α : Type u_1} {s : Set α} : EventuallyEmptyOrUniv s ⊥

theorem Filter.EventuallyEmptyOrUniv.congr {α : Type u_1} {l : Filter α} {s t : Set α} (h : EventuallyEmptyOrUniv s l) (hst : s =ᶠ[l] t) : EventuallyEmptyOrUniv t l

theorem Filter.EventuallyEmptyOrUniv.anti {α : Type u_1} {l : Filter α} {s : Set α} {l' : Filter α} (h : EventuallyEmptyOrUniv s l) (hl' : l' ≤ l) : EventuallyEmptyOrUniv s l'

theorem Filter.EventuallyEmptyOrUniv.of_mulIndicator_const {α : Type u_1} {β : Type u_2} {l : Filter α} [One β] {s : Set α} {c : β} (h : EventuallyConst (s.mulIndicator fun (x : α) => c) l) (hc : c ≠ 1) : EventuallyEmptyOrUniv s l

theorem Filter.EventuallyEmptyOrUniv.of_indicator_const {α : Type u_1} {β : Type u_2} {l : Filter α} [Zero β] {s : Set α} {c : β} (h : EventuallyConst (s.indicator fun (x : α) => c) l) (hc : c ≠ 0) : EventuallyEmptyOrUniv s l

theorem Filter.EventuallyEmptyOrUniv.mulIndicator_const {α : Type u_1} {β : Type u_2} {l : Filter α} [One β] {s : Set α} (h : EventuallyEmptyOrUniv s l) (c : β) : EventuallyConst (s.mulIndicator fun (x : α) => c) l

theorem Filter.EventuallyEmptyOrUniv.indicator_const {α : Type u_1} {β : Type u_2} {l : Filter α} [Zero β] {s : Set α} (h : EventuallyEmptyOrUniv s l) (c : β) : EventuallyConst (s.indicator fun (x : α) => c) l

theorem Filter.EventuallyEmptyOrUniv.mulIndicator_const_iff_of_ne {α : Type u_1} {β : Type u_2} {l : Filter α} [One β] {s : Set α} {c : β} (hc : c ≠ 1) : EventuallyConst (s.mulIndicator fun (x : α) => c) l ↔ EventuallyEmptyOrUniv s l

theorem Filter.EventuallyEmptyOrUniv.indicator_const_iff_of_ne {α : Type u_1} {β : Type u_2} {l : Filter α} [Zero β] {s : Set α} {c : β} (hc : c ≠ 0) : EventuallyConst (s.indicator fun (x : α) => c) l ↔ EventuallyEmptyOrUniv s l

@[simp]

theorem Filter.EventuallyEmptyOrUniv.mulIndicator_const_iff {α : Type u_1} {β : Type u_2} {l : Filter α} [One β] {s : Set α} {c : β} : EventuallyConst (s.mulIndicator fun (x : α) => c) l ↔ c = 1 ∨ EventuallyEmptyOrUniv s l

@[simp]

theorem Filter.EventuallyEmptyOrUniv.indicator_const_iff {α : Type u_1} {β : Type u_2} {l : Filter α} [Zero β] {s : Set α} {c : β} : EventuallyConst (s.indicator fun (x : α) => c) l ↔ c = 0 ∨ EventuallyEmptyOrUniv s l

@[deprecated Filter.EventuallyEmptyOrUniv.of_mulIndicator_const (since := "2026-08-25")]

theorem Filter.EventuallyConst.of_mulIndicator_const {α : Type u_1} {β : Type u_2} {l : Filter α} [One β] {s : Set α} {c : β} (h : EventuallyConst (s.mulIndicator fun (x : α) => c) l) (hc : c ≠ 1) : EventuallyConst s l

@[deprecated Filter.EventuallyEmptyOrUniv.of_indicator_const (since := "2026-08-25")]

theorem Filter.EventuallyConst.of_indicator_const {α : Type u_1} {β : Type u_2} {l : Filter α} [Zero β] {s : Set α} {c : β} (h : EventuallyConst (s.indicator fun (x : α) => c) l) (hc : c ≠ 0) : EventuallyConst s l

@[deprecated Filter.EventuallyEmptyOrUniv.mulIndicator_const (since := "2026-08-25")]

theorem Filter.EventuallyConst.mulIndicator_const {α : Type u_1} {β : Type u_2} {l : Filter α} [One β] {s : Set α} (h : EventuallyConst s l) (c : β) : EventuallyConst (s.mulIndicator fun (x : α) => c) l

@[deprecated Filter.EventuallyEmptyOrUniv.indicator_const (since := "2026-08-25")]

theorem Filter.EventuallyConst.indicator_const {α : Type u_1} {β : Type u_2} {l : Filter α} [Zero β] {s : Set α} (h : EventuallyConst s l) (c : β) : EventuallyConst (s.indicator fun (x : α) => c) l

@[deprecated Filter.EventuallyEmptyOrUniv.mulIndicator_const_iff_of_ne (since := "2026-08-25")]

theorem Filter.EventuallyConst.mulIndicator_const_iff_of_ne {α : Type u_1} {β : Type u_2} {l : Filter α} [One β] {s : Set α} {c : β} (hc : c ≠ 1) : EventuallyConst (s.mulIndicator fun (x : α) => c) l ↔ EventuallyConst s l

@[deprecated Filter.EventuallyEmptyOrUniv.indicator_const_iff_of_ne (since := "2026-08-25")]

theorem Filter.EventuallyConst.indicator_const_iff_of_ne {α : Type u_1} {β : Type u_2} {l : Filter α} [Zero β] {s : Set α} {c : β} (hc : c ≠ 0) : EventuallyConst (s.indicator fun (x : α) => c) l ↔ EventuallyConst s l

@[deprecated Filter.EventuallyEmptyOrUniv.mulIndicator_const_iff (since := "2026-08-25")]

theorem Filter.EventuallyConst.mulIndicator_const_iff {α : Type u_1} {β : Type u_2} {l : Filter α} [One β] {s : Set α} {c : β} : EventuallyConst (s.mulIndicator fun (x : α) => c) l ↔ c = 1 ∨ EventuallyConst s l

@[deprecated Filter.EventuallyEmptyOrUniv.indicator_const_iff (since := "2026-08-25")]

theorem Filter.EventuallyConst.indicator_const_iff {α : Type u_1} {β : Type u_2} {l : Filter α} [Zero β] {s : Set α} {c : β} : EventuallyConst (s.indicator fun (x : α) => c) l ↔ c = 0 ∨ EventuallyConst s l

theorem Filter.eventuallyConst_atTop {α : Type u_1} {β : Type u_2} {f : α → β} [SemilatticeSup α] [Nonempty α] : EventuallyConst f atTop ↔ ∃ (i : α), ∀ (j : α), i ≤ j → f j = f i

theorem Filter.eventuallyConst_atTop_nat {α : Type u_1} {f : ℕ → α} : EventuallyConst f atTop ↔ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = f m