top_le_iff — Mathlib

English

For every a ∈ WithTop(α), ⊤ ≤ a if and only if a = ⊤.

Русский

Для любого a ∈ WithTop(α), ⊤ ≤ a тогда и только тогда, когда a = ⊤.

LaTeX

$$$\forall a : \mathrm{WithTop}(\alpha),\ \top \le a \iff a = \top$$$

Lean4

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

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