val_le_val — Mathlib

English

The embedding val respects order: for any a,b in Units α, (a:α) ≤ b if and only if a ≤ b in Units α.

Русский

Встроенная карта val сохраняет порядок: для любых a,b из Units α выполняется (a:α) ≤ b ⇔ a ≤ b в Units α.

LaTeX

$$$\\forall {a,b \\in \\mathrm{Units}(\\alpha)},\\ (a : \\alpha) \\le b \\iff a \\le b$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem val_le_val [Monoid α] [Preorder α] {a b : αˣ} : (a : α) ≤ b ↔ a ≤ b :=
  Iff.rfl

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