iInter_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 intersections over the indices are equal: ⋂_x f(x) = ⋂_y g(y).

Русский

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

LaTeX

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

Lean4

theorem iInter_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.iInf_congr h h2

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