sSup_diff_singleton_bot — Mathlib

English

Let α be a complete lattice with bottom element ⊥. For any subset s ⊆ α, removing the bottom element does not change its supremum: sSup(s \ {⊥}) = sSup(s).

Русский

Пусть α — полная решётка с нулём ⊥. Для любого подмножества s ⊆ α верно, что верхняя граница множества, полученного удалением нижнего элемента, не изменяется: sSup(s \ {⊥}) = sSup(s).

LaTeX

$$$$ \operatorname{sSup}(s \setminus \{ \bot \}) = \operatorname{sSup}(s) $$$$

Lean4

@[simp]
theorem sSup_diff_singleton_bot (s : Set α) : sSup (s \ {⊥}) = sSup s :=
  (sSup_le_sSup diff_subset).antisymm <| sSup_le_sSup_of_subset_insert_bot <| subset_insert_diff_singleton _ _

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