one_le_coe — Mathlib

English

One is less than or equal to the embedded element in WithBot α, if and only if 1 ≤ a in α.

Русский

Единица не превосходит встроенный элемент в WithBot α тогда и только тогда, когда 1 ≤ a в α.

LaTeX

$$$ 1 \\le (a : \\mathrm{WithBot}\\,\\alpha) \\iff 1 \\le a $$$

Lean4

@[to_additive (attr := simp, norm_cast) coe_nonneg]
theorem one_le_coe [LE α] : 1 ≤ (a : WithBot α) ↔ 1 ≤ a :=
  coe_le_coe

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