iUnion_comp — Mathlib

English

If f : ι → ι₂ is surjective, then the union over x of g(f(x)) equals the union over y of g(y).

Русский

Пусть f : ι → ι₂ сюръективна. Тогда объединение по x ∈ ι of g(f(x)) равно объединению по y ∈ ι₂ of g(y).

LaTeX

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

Lean4

theorem iUnion_comp {f : ι → ι₂} (hf : Surjective f) (g : ι₂ → Set α) : ⋃ x, g (f x) = ⋃ y, g y :=
  hf.iSup_comp g

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