adjoin_attach_biUnion — Mathlib

English

For a Finset α and f: α-attached Finsets → Set A, adjoin of the biUnion equals the supremum over α of adjoin of each f x.

Русский

Для конечного множества α и отображения f: α → Finset A, adjoin знака biUnion равен наибольшему верхнему пределу adjoin всех f x.

LaTeX

$$$\\operatorname{adjoin}^R\\bigl( (\\mathrm{attach}.biUnion f) \\bigr) = \\bigvee_x \\operatorname{adjoin}^R (f x)$$$

Lean4

theorem adjoin_attach_biUnion [DecidableEq A] {α : Type*} {s : Finset α} (f : s → Finset A) :
    adjoin R (s.attach.biUnion f : Set A) = ⨆ x, adjoin R (f x) := by simp [adjoin_iUnion]

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