lt_def — Mathlib

English

The strict order lt is defined componentwise by the base order on β; i.e., f < g iff ∀ a, f(a) ≤ g(a) and ∃ a, f(a) < g(a).

Русский

Строгое неравенство задаётся компонентно по базовому порядку β: ∀ 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 {f g : C_c(α, β)} : f < g ↔ (∀ a, f a ≤ g a) ∧ ∃ a, f a < g a :=
  Pi.lt_def

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