iUnion_congr_of_surjective — Mathlib

English

Let f: I → Set α and g: I2 → Set α. If h: I → I2 is surjective and g(h(x)) = f(x) for all x, then the unions over the indices are equal: ⋃_x f(x) = ⋃_y g(y).

Русский

Пусть f: I → Set α и g: I2 → Set α. Если h: I → I2 сюръективен и для всех x выполняется g(h(x)) = f(x), то ⋃_x f(x) = ⋃_y g(y).

LaTeX

$$$$ \\left( \\forall x,\, g(h(x)) = f(x) \\right) \\Rightarrow \\bigcup_{x} f(x) = \\bigcup_{y} g(y) $$$$

Lean4

theorem iUnion_congr_of_surjective {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂) (h1 : Surjective h)
    (h2 : ∀ x, g (h x) = f x) : ⋃ x, f x = ⋃ y, g y :=
  h1.iSup_congr h h2

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