iInter_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iInter_comp {f : ι → ι₂} (hf : Surjective f) (g : ι₂ → Set α) : ⋂ x, g (f x) = ⋂ y, g y :=
  hf.iInf_comp g

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