set_biInter_finset_image — Mathlib

English

Intersection over the image of a finite set s under f with family g equals the intersection over s of g(f(y)).

Русский

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

LaTeX

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

Lean4

theorem set_biInter_finset_image {f : γ → α} {g : α → Set β} {s : Finset γ} : ⋂ x ∈ s.image f, g x = ⋂ y ∈ s, g (f y) :=
  iInf_finset_image

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