sSup_eq_bot — Mathlib

English

In a complete lattice with bottom ⊥, the supremum of a set s equals ⊥ if and only if every element of s is ⊥.

Русский

В полной решётке с нижним элементом ⊥ супремум множества s равен ⊥ тогда и только тогда, когда каждый элемент s равен ⊥.

LaTeX

$$$$ \operatorname{sSup} s = \bot \iff \forall a \in s, a = \bot $$$$

Lean4

@[simp]
theorem sSup_eq_bot : sSup s = ⊥ ↔ ∀ a ∈ s, a = ⊥ :=
  ⟨fun h _ ha => bot_unique <| h ▸ le_sSup ha, fun h => bot_unique <| sSup_le fun a ha => le_bot_iff.2 <| h a ha⟩

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