sSup_eq_bot' — Mathlib

English

For any s ⊆ α, sSup s = ⊥ implies s = ∅ or s = {⊥}. Equivalently, sSup s = ⊥ if and only if s = ∅ or s = {⊥}.

Русский

Для любого множества s, если sSup s = ⊥, то s равно пустому множеству или {⊥}. Аналогично, если s = ∅ или s = {⊥}, то sSup s = ⊥.

LaTeX

$$$$ \operatorname{sSup} s = \bot \iff s = \emptyset \lor s = \{\bot\} $$$$

Lean4

theorem sSup_eq_bot' {s : Set α} : sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥} := by
  rw [sSup_eq_bot, ← subset_singleton_iff_eq, subset_singleton_iff]

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