eventuallyConst_pred' — Mathlib

English

For nonempty β, EventuallyConst f l is equivalent to the existence of x with Tendsto f l (pure x).

Русский

Для непустого β условие EventuallyConst f l эквивалентно существованию x, при котором Tendsto f l (pure x).

LaTeX

$$$\\\\forall {f} {l} [Nonempty B],\\\\; (EventuallyConst f l) \\\\Leftrightarrow \\\\exists x, Tendsto f l (\\\\text{pure } x)$$$

Lean4

theorem eventuallyConst_pred' {p : α → Prop} : EventuallyConst p l ↔ (p =ᶠ[l] fun _ ↦ False) ∨ (p =ᶠ[l] fun _ ↦ True) :=
  by simp only [eventuallyConst_iff_exists_eventuallyEq, «Prop».exists_iff]

Похожие утверждения