coe_eq_bot — Mathlib

English

If α has a bottom element, then for any a ∈ α, (a in WithTop α) equals ⊥ if and only if a equals ⊥.

Русский

Пусть в α есть нижний элемент; тогда для любого a: α, (a в WithTop(α)) равно ⊥ тогда и только тогда, когда a = ⊥.

LaTeX

$$$(a : \mathrm{WithTop}(\alpha)) = \bot \iff a = \bot$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_bot [Bot α] {a : α} : (a : WithTop α) = ⊥ ↔ a = ⊥ :=
  coe_eq_coe

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