sup_bot — Mathlib

English

In a semilattice with bottom, the supremum over any finite set of the bottom element ⊥ is ⊥.

Русский

В полупорядованный множестве с нижней границей элементом является ⊥; супремум по любому конечному множеству от ⊥ равен ⊥.

LaTeX

$$$\displaystyle \forall s,\ (s.sup (\lambda \_ : \text{β}, \bot)) = \bot$$$

Lean4

@[simp]
theorem sup_bot (s : Finset β) : (s.sup fun _ => ⊥) = (⊥ : α) :=
  by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · exact sup_empty
  · exact sup_const hs _

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