const_eventuallyEq — Mathlib

English

For any l with l ≠⊥, the constant functions a and b are eventually equal along l if and only if a = b.

Русский

Для ненулевого фильтра l константные функции a и b равны вдоль l в смысле равенства «в конечном счёте» тогда и только если a=b.

LaTeX

$$$[l \text{ NeBot}]\; (l.}\mathrm{EventuallyEq} (\lambda x. a) (\lambda x. b) \iff a = b.$$$

Lean4

theorem const_eventuallyEq [NeBot l] {a b : β} : ((fun _ => a) =ᶠ[l] fun _ => b) ↔ a = b :=
  @const_eventuallyEq' _ _ _ _ a b

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