set_biUnion_finset_image — Mathlib

English

Union over the image of a finite set s under function f, composed with a family g, equals the union over s of g(f(y)).

Русский

Объединение по образу конечного множества s через отображение f и семейство g равно объединению по s с g(f(y)).

LaTeX

$$$$ \\bigcup_{x \\in s.image f} g(x) = \\bigcup_{y \\in s} g(f(y)) $$$$

Lean4

theorem set_biUnion_finset_image {f : γ → α} {g : α → Set β} {s : Finset γ} : ⋃ x ∈ s.image f, g x = ⋃ y ∈ s, g (f y) :=
  iSup_finset_image

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