lt_def — Mathlib

English

For f,g ∈ C(α, β) with β partially ordered, f < g iff (∀ a, f(a) ≤ g(a)) and there exists a with f(a) < g(a).

Русский

Для f,g ∈ C(α, β) верно: f < g тогда и только тогда, когда ∀ a, f(a) ≤ g(a) и существует a такой, что f(a) < g(a).

LaTeX

$$\$f < g \\iff (\\forall a, f(a) \\le g(a)) \\land \\exists a, f(a) < g(a)\$.$$

Lean4

theorem lt_def [PartialOrder β] {f g : C(α, β)} : f < g ↔ (∀ a, f a ≤ g a) ∧ ∃ a, f a < g a :=
  Pi.lt_def

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