lowerBounds_iUnion — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem lowerBounds_iUnion : lowerBounds (⋃ i, s i) = ⋂ i, lowerBounds (s i) :=
  gc_upperBounds_lowerBounds.u_iInf

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