English
If f is injective on the union of s_i, then the image of the intersection equals the intersection of the images.
Русский
Если f инъективно на объединении s_i, то образ пересечения равен пересечению образов.
LaTeX
$$$\\text{image iInter}$ with InjOn f on union implies $$f(\\cap_i s_i) = \\cap_i f(s_i).$$$$
Lean4
theorem image_iInter_eq [Nonempty ι] {s : ι → Set α} {f : α → β} (h : InjOn f (⋃ i, s i)) :
(f '' ⋂ i, s i) = ⋂ i, f '' s i := by
inhabit ι
refine Subset.antisymm (image_iInter_subset s f) fun y hy => ?_
simp only [mem_iInter, mem_image] at hy
choose x hx hy using hy
refine ⟨x default, mem_iInter.2 fun i => ?_, hy _⟩
suffices x default = x i by
rw [this]
apply hx
replace hx : ∀ i, x i ∈ ⋃ j, s j := fun i => (subset_iUnion _ _) (hx i)
apply h (hx _) (hx _)
simp only [hy]
