Documentation

Mathlib.Order.Filter.EventuallyConst

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 : Filter α) :

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

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