eventuallyConst_iff — Mathlib

English

If f is eventually equal to g along l, then f is eventually constant along l iff g is.

Русский

Если f и g равны по л, тогда константность f и g эквивалентны.

LaTeX

$$$\\\\forall {f g} (h : f =\\\\^l g), \\\\; EventuallyConst f l \\\\Leftrightarrow EventuallyConst g l$$$

Lean4

theorem eventuallyConst_iff {g : α → β} (h : f =ᶠ[l] g) : EventuallyConst f l ↔ EventuallyConst g l := by
  simp only [EventuallyConst, map_congr h]

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