adjoin_iUnion — Mathlib

English

For a family of sets f(i) ⊆ E, the adjoin of their union equals the supremum of the adjoins: adjoin F (⋃ i, f(i)) = ⨆ i, adjoin F (f(i)).

Русский

Для семейства множеств f(i) ⊆ E адъюнт объединения равен верхней грани над адъюнтами: adjoin F (⋃ i, f(i)) = ⨆ i, adjoin F (f(i)).

LaTeX

$$$\\\\operatorname{adjoin}_F (\\\\bigcup_i f(i)) = \\\\bigvee_i \\\\operatorname{adjoin}_F (f(i)).$$$

Lean4

theorem adjoin_iUnion {ι} (f : ι → Set E) : adjoin F (⋃ i, f i) = ⨆ i, adjoin F (f i) :=
  gc.l_iSup

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