# 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.

## 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 : ) :

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

Equations
• = ().Subsingleton
Instances For
theorem Filter.HasBasis.eventuallyConst_iff {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {ι : Sort u_5} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) :
∃ (i : ι), p i xs i, ys i, f x = f y
theorem Filter.HasBasis.eventuallyConst_iff' {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {ι : Sort u_5} {p : ιProp} {s : ιSet α} {x : ια} (h : l.HasBasis p s) (hx : ∀ (i : ι), p ix i s i) :
∃ (i : ι), p i ys i, f y = f (x i)
theorem Filter.eventuallyConst_iff_tendsto {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [] :
∃ (x : β), Filter.Tendsto f l (pure x)
theorem Filter.EventuallyConst.exists_tendsto {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [] :
∃ (x : β), Filter.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 : } {f : αβ} {x : β} (h : Filter.Tendsto f l (pure x)) :
theorem Filter.eventuallyConst_iff_exists_eventuallyEq {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [] :
∃ (c : β), f =ᶠ[l] fun (x : α) => c
theorem Filter.EventuallyConst.eventuallyEq_const {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [] :
∃ (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 : } {p : αProp} :
(p =ᶠ[l] fun (x : α) => False) p =ᶠ[l] fun (x : α) => True
theorem Filter.eventuallyConst_pred {α : Type u_1} {l : } {p : αProp} :
(∀ᶠ (x : α) in l, p x) ∀ᶠ (x : α) in l, ¬p x
theorem Filter.eventuallyConst_set' {α : Type u_1} {l : } {s : Set α} :
s =ᶠ[l] s =ᶠ[l] Set.univ
theorem Filter.eventuallyConst_set {α : Type u_1} {l : } {s : Set α} :
(∀ᶠ (x : α) in l, x s) ∀ᶠ (x : α) in l, xs
theorem Filter.EventuallyEq.eventuallyConst_iff {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {g : αβ} (h : f =ᶠ[l] g) :
@[simp]
theorem Filter.eventuallyConst_id {α : Type u_1} {l : } :
l.Subsingleton
@[simp]
theorem Filter.EventuallyConst.bot {α : Type u_1} {β : Type u_2} {f : αβ} :
@[simp]
theorem Filter.EventuallyConst.const {α : Type u_1} {β : Type u_2} {l : } (c : β) :
Filter.EventuallyConst (fun (x : α) => c) l
theorem Filter.EventuallyConst.congr {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {g : αβ} (h : ) (hg : f =ᶠ[l] g) :
theorem Filter.EventuallyConst.of_subsingleton_right {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [] :
theorem Filter.EventuallyConst.anti {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {l' : } (h : ) (hl' : l' l) :
theorem Filter.EventuallyConst.of_subsingleton_left {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [] :
theorem Filter.EventuallyConst.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } {f : αβ} (h : ) (g : βγ) :
theorem Filter.EventuallyConst.neg {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [Neg β] (h : ) :
theorem Filter.EventuallyConst.inv {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [Inv β] (h : ) :
theorem Filter.EventuallyConst.comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } {f : αβ} {lb : } {g : βγ} (hg : ) (hf : Filter.Tendsto f l lb) :
theorem Filter.EventuallyConst.apply {α : Type u_1} {l : } {ι : Type u_5} {p : ιType u_6} {g : α(x : ι) → p x} (h : ) (i : ι) :
Filter.EventuallyConst (fun (x : α) => g x i) l
theorem Filter.EventuallyConst.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : } {f : αβ} {g : αγ} (hf : ) (op : βγδ) (hg : ) :
Filter.EventuallyConst (fun (x : α) => op (f x) (g x)) l
theorem Filter.EventuallyConst.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } {f : αβ} {g : αγ} (hf : ) (hg : ) :
Filter.EventuallyConst (fun (x : α) => (f x, g x)) l
theorem Filter.EventuallyConst.add {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [Add β] {g : αβ} (hf : ) (hg : ) :
theorem Filter.EventuallyConst.mul {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [Mul β] {g : αβ} (hf : ) (hg : ) :
theorem Filter.EventuallyConst.of_indicator_const {α : Type u_1} {β : Type u_2} {l : } [Zero β] {s : Set α} {c : β} (h : Filter.EventuallyConst (s.indicator fun (x : α) => c) l) (hc : c 0) :
theorem Filter.EventuallyConst.of_mulIndicator_const {α : Type u_1} {β : Type u_2} {l : } [One β] {s : Set α} {c : β} (h : Filter.EventuallyConst (s.mulIndicator fun (x : α) => c) l) (hc : c 1) :
theorem Filter.EventuallyConst.indicator_const {α : Type u_1} {β : Type u_2} {l : } [Zero β] {s : Set α} (h : ) (c : β) :
Filter.EventuallyConst (s.indicator fun (x : α) => c) l
theorem Filter.EventuallyConst.mulIndicator_const {α : Type u_1} {β : Type u_2} {l : } [One β] {s : Set α} (h : ) (c : β) :
Filter.EventuallyConst (s.mulIndicator fun (x : α) => c) l
theorem Filter.EventuallyConst.indicator_const_iff_of_ne {α : Type u_1} {β : Type u_2} {l : } [Zero β] {s : Set α} {c : β} (hc : c 0) :
Filter.EventuallyConst (s.indicator fun (x : α) => c) l
theorem Filter.EventuallyConst.mulIndicator_const_iff_of_ne {α : Type u_1} {β : Type u_2} {l : } [One β] {s : Set α} {c : β} (hc : c 1) :
Filter.EventuallyConst (s.mulIndicator fun (x : α) => c) l
@[simp]
theorem Filter.EventuallyConst.indicator_const_iff {α : Type u_1} {β : Type u_2} {l : } [Zero β] {s : Set α} {c : β} :
Filter.EventuallyConst (s.indicator fun (x : α) => c) l c = 0
@[simp]
theorem Filter.EventuallyConst.mulIndicator_const_iff {α : Type u_1} {β : Type u_2} {l : } [One β] {s : Set α} {c : β} :
Filter.EventuallyConst (s.mulIndicator fun (x : α) => c) l c = 1
theorem Filter.eventuallyConst_atTop {α : Type u_1} {β : Type u_2} {f : αβ} [] [] :
Filter.EventuallyConst f Filter.atTop ∃ (i : α), ∀ (j : α), i jf j = f i
theorem Filter.eventuallyConst_atTop_nat {α : Type u_1} {f : α} :
Filter.EventuallyConst f Filter.atTop ∃ (n : ), ∀ (m : ), n mf (m + 1) = f m