congr — Mathlib

English

If f is EventuallyConst along l and f =ᶠ[l] g, then g is EventuallyConst along l.

Русский

Если f является EventuallyConst вдоль l и f эквивалентно g по мере l, то g также является EventuallyConst вдоль l.

LaTeX

$$$\mathrm{EventuallyConst}(f,l) \land f =^l g \Rightarrow \mathrm{EventuallyConst}(g,l)$$$

Lean4

protected theorem congr {g} (h : EventuallyConst f l) (hg : f =ᶠ[l] g) : EventuallyConst g l :=
  hg.eventuallyConst_iff.1 h

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