le_coe_iff — Mathlib

English

Let x be an element of WithBot α and b an element of α. Then x ≤ b in WithBot α if and only if, for every a ∈ α, whenever x equals the embedding of a, we have a ≤ b.

Русский

Пусть x ∈ WithBot α и b ∈ α. Тогда x ≤ b в WithBot α эквивалентно тому, что для всякого a ∈ α, если x равен образу a, то a ≤ b.

LaTeX

$$$ x \le \iota(b) \iff \forall a : \alpha, x = \iota(a) \rightarrow a \le b $$$

Lean4

theorem le_coe_iff : x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b := by simp [le_def]

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