image_iInter — Mathlib

English

If f is bijective, then the image of an intersection equals the intersection of images, with a caveat for nonempty index sets.

Русский

Если отображение биективно, то образ пересечения равен пересечению образов (при ненулевом индексе).

LaTeX

$$$\\text{image iInter}$$$

Lean4

theorem image_iInter {f : α → β} (hf : Bijective f) (s : ι → Set α) : (f '' ⋂ i, s i) = ⋂ i, f '' s i :=
  by
  cases isEmpty_or_nonempty ι
  · simp_rw [iInter_of_empty, image_univ_of_surjective hf.surjective]
  · exact hf.injective.injOn.image_iInter_eq

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