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