adjoin_iUnion — Mathlib

English

The adjoin of the union equals the supremum of the adjoins: adjoin R (Set.iUnion s) = ⨆ i, adjoin R (s i).

Русский

Объединение адайона равно наибольшему верхнему пределу адайонов: adjoin R (⋃_i s_i) = ⨆_i adjoin R (s_i).

LaTeX

$$$\\operatorname{adjoin}^R(\\bigcup_i s_i) = \\bigvee_i \\operatorname{adjoin}^R(s_i)$$$

Lean4

theorem adjoin_iUnion {α : Type*} (s : α → Set A) : adjoin R (Set.iUnion s) = ⨆ i : α, adjoin R (s i) :=
  (@Algebra.gc R A _ _ _).l_iSup

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