coe_sSup — Mathlib

English

The underlying set of the supremum of a set S of UpperSets is the intersection over all s ∈ S of the underlying sets of s.

Русский

Носитель наибольшего элемента множества S верхних множеств равен пересечению носителей каждого s ∈ S.

LaTeX

$$↑(sSup S) = ⋂ s ∈ S, ↑s$$

Lean4

@[simp, norm_cast]
theorem coe_sSup (S : Set (UpperSet α)) : (↑(sSup S) : Set α) = ⋂ s ∈ S, ↑s :=
  rfl

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