le_def — Mathlib

English

For any x,y in WithZero α, x ≤ y if and only if for every a ∈ α with x = ↑a there exists b ∈ α with y = ↑b and a ≤ b.

Русский

Для любых x,y ∈ WithZero α верно: x ≤ y тогда и только тогда, когда для любого a ∈ α, если x = ↑a, существует b ∈ α, такое что y = ↑b и a ≤ b.

LaTeX

$$$x \\le y \\\\iff \\\\forall a \\in \\\\alpha, x = \\uparrow a \\\\Rightarrow \\\\exists b \\in \\\\alpha, y = \\uparrow b \\\\land a \\le b$$$

Lean4

theorem le_def : x ≤ y ↔ ∀ a : α, x = ↑a → ∃ b : α, y = ↑b ∧ a ≤ b :=
  .rfl

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