coe_lt — Mathlib

English

For f,g: α → β, the order in the germ β* satisfies f < g if and only if f(x) < g(x) eventually (for φ-almost all x).

Русский

Для функций f,g: α → β порядок в Germ β* определяется тем, что f < g тогда и только тогда, когда f(x) < g(x) происходит для почти всех x (по исключению φ).

LaTeX

$$$(f : β^*) < g \\iff \\forall^* x,\\ f(x) < g(x).$$$

Lean4

theorem coe_lt [Preorder β] {f g : α → β} : (f : β*) < g ↔ ∀* x, f x < g x := by
  simp only [lt_iff_le_not_ge, eventually_and, coe_le, eventually_not, EventuallyLE]

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