ne_of_lt — Mathlib

English

If f(x) < g(x) holds eventually along l, then f(x) ≠ g(x) also holds eventually along l.

Русский

Если неравенство f(x) < g(x) выполняется почти наверное вдоль l, то неравенство f(x) ≠ g(x) тоже выполняется почти наверху вдоль l.

LaTeX

$$$ (∀ᶠ x in l, f x < g x) \\Rightarrow (∀ᶠ x in l, f x ≠ g x) $$$

Lean4

theorem ne_of_lt [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ᶠ x in l, f x < g x) : ∀ᶠ x in l, f x ≠ g x :=
  h.mono fun _ hx => hx.ne

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