not_bot_lt_iff — Mathlib

English

Let A be a partially ordered set with a bottom element ⊥. Then for every a in A, ⊥ < a holds exactly when a ≠ ⊥; equivalently, ¬(⊥ < a) ⇔ a = ⊥.

Русский

Пусть A — частично упорядченное множество с минимальным элементом ⊥. Тогда для любого a ∈ A неравенство ⊥ < a эквивалентно тому, что a ≠ ⊥; то есть ¬(⊥ < a) ⇔ a = ⊥.

LaTeX

$$$\neg (\bot < a) \iff a = \bot$$$

Lean4

@[simp]
theorem not_bot_lt_iff : ¬⊥ < a ↔ a = ⊥ :=
  bot_lt_iff_ne_bot.not_left

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