eq_bot_iff_forall_ne — Mathlib

English

An element x of WithBot α equals ⊥ if and only if every a ∈ α satisfies a ≠ x in the sense of coe.

Русский

Элемент x из WithBot α равен ⊥ тогда, когда для каждого a ∈ α выполняется a ≠ x в терминах вставки.

LaTeX

$$$x = \bot \iff \forall a : α, \uparrow a \neq x$$$

Lean4

theorem eq_bot_iff_forall_ne {x : WithBot α} : x = ⊥ ↔ ∀ a : α, ↑a ≠ x :=
  Option.eq_none_iff_forall_some_ne

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