le_bot_iff — Mathlib

English

There is a simple lemma: for any a in WithBot α, a ≤ ⊥ iff a = ⊥.

Русский

Существует простая лемма: для любого a ∈ WithBot α, a ≤ ⊥ эквивалентно a = ⊥.

LaTeX

$$$\forall {a : WithBot α}, a \le \bot \leftrightarrow a = \bot$$$

Lean4

/-- There is a general version `le_bot_iff`, but this lemma does not require a `PartialOrder`. -/
@[simp]
protected theorem le_bot_iff : ∀ {a : WithBot α}, a ≤ ⊥ ↔ a = ⊥
  | (a : α) => by simp [not_coe_le_bot _]
  | ⊥ => by simp

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