eq_singleton_bot_of_sSup_eq_bot_of_nonempty

English

If s is nonempty and its supremum is ⊥, then s = {⊥}.

Русский

Если s непусто и его супремум равен ⊥, то s = {⊥}.

LaTeX

$$$$ sSup s = \bot \Rightarrow s \text{ Nonempty } \Rightarrow s = \{ \bot \} $$$$

Lean4

theorem eq_singleton_bot_of_sSup_eq_bot_of_nonempty {s : Set α} (h_sup : sSup s = ⊥) (hne : s.Nonempty) : s = {⊥} :=
  by
  rw [Set.eq_singleton_iff_nonempty_unique_mem]
  rw [sSup_eq_bot] at h_sup
  exact ⟨hne, h_sup⟩

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