le — Mathlib · SciLib

English

The order on WithZero α is defined by o1 ≤ o2 if and only if there exist a,b ∈ α with o1 = ↑a, o2 = ↑b and a ≤ b.

Русский

Порядок на WithZero α задаётся так: o1 ≤ o2 тогда и только тогда, когда существуют a,b ∈ α с o1 = ↑a, o2 = ↑b и a ≤ b.

LaTeX

$$$o_1 \\le o_2 \\iff \\exists a,b \\in \\alpha,\\ o_1 = \\uparrow a \\\\land o_2 = \\uparrow b \\\\land a \\le b$$$

Lean4

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

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