English
If f is injective, then the previous subset becomes equality.
Русский
Если f инъективен, то вложение превращается в равенство.
LaTeX
$$$\\text{Injective } f \\Rightarrow\\ (\\\\Sigma.mk i '' (g i^{-1}' s) = (\\\\Sigma.map f g)^{-1}' (\\\\Sigma.mk (f i) '' s))$$$
Lean4
theorem image_sigmaMk_preimage_sigmaMap {β : ι' → Type*} {f : ι → ι'} (hf : Function.Injective f)
(g : ∀ i, α i → β (f i)) (i : ι) (s : Set (β (f i))) :
Sigma.mk i '' (g i ⁻¹' s) = Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s) :=
by
refine (image_sigmaMk_preimage_sigmaMap_subset f g i s).antisymm ?_
rintro ⟨j, x⟩ ⟨y, hys, hxy⟩
simp only [hf.eq_iff, Sigma.map, Sigma.ext_iff] at hxy
grind