coe_le_iff — Mathlib

English

For x ∈ WithZero α and a ∈ α, x ≤ a is equivalent to there existing b with x = ↑b and a ≥ b.

Русский

Для x ∈ WithZero α и a ∈ α, x ≤ a эквивалентно существованию b, такого что x = ↑b и a ≥ b.

LaTeX

$$$ (a : \mathrm{WithZero} \alpha) \le x \iff \exists b : \alpha, x = \uparrow b \land a \le b $$$

Lean4

theorem coe_le_iff {x : WithZero α} : (a : WithZero α) ≤ x ↔ ∃ b : α, x = b ∧ a ≤ b := by simp [le_def]

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