lt — Mathlib · SciLib

English

The less-than relation on WithZero α is defined by o1 < o2 if and only if there exists b with o2 = ↑b and for all a with o1 = ↑a one has a < b.

Русский

Отношение меньшего на WithZero α задаётся так: o1 < o2 тогда и только тогда, когда существует b, такое что o2 = ↑b и для всех a, если o1 = ↑a, то a < b.

LaTeX

$$$o_1 < o_2 \\iff \\exists b \\in \\alpha,\\ o_2 = \\uparrow b \\\\land \\forall a \\\\in \\alpha, o_1 = \\uparrow a \\Rightarrow a < b$$$

Lean4

instance (priority := 10) lt : LT (WithZero α) :=
  ⟨fun o₁ o₂ : WithZero α => ∃ b : α, o₂ = ↑b ∧ ∀ a : α, o₁ = ↑a → a < b⟩

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