upperBounds_iUnion — Mathlib

English

Let α be a preorder and (s_i) a family of subsets of α. Then the upper bounds of the union equal the intersection of the upper bounds: upperBounds(⋃_i s_i) = ⋂_i upperBounds(s_i).

Русский

Пусть A—частично упорядованное множество, и {s_i} — семейство подмножеств A. Тогда верхние границы объединения равны пересечению верхних границ: upperBounds(⋃_i s_i) = ⋂_i upperBounds(s_i).

LaTeX

$$$\\operatorname{upperBounds}\\left(\\bigcup_i s_i\\right) = \\bigcap_i \\operatorname{upperBounds}(s_i).$$$

Lean4

@[simp]
theorem upperBounds_iUnion : upperBounds (⋃ i, s i) = ⋂ i, upperBounds (s i) :=
  gc_upperBounds_lowerBounds.l_iSup

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