English
The preimage of a subset u under the left-inverse map equals the preimage of f applied to u under the right map, i.e., the inverse image corresponds under the image bijection.
Русский
Первообразное подмножества u под соответствием левой обратнообразующей карты равно первообразному подмножества f''u под соответствием правой карты.
LaTeX
$$$\\big(\\mathrm{Set.preimage} (\\lambda x. (\\mathrm{Set.image} f\, s\, H).symm\\, x)\\; u\\big) = \\mathrm{Set.preimage}\\, \\mathrm{Subtype.val} \\, (\\mathrm{Set.image} f\, u)$$$
Lean4
theorem image_symm_preimage {α β} {f : α → β} (hf : Injective f) (u s : Set α) :
(fun x => (Set.image f s hf).symm x : f '' s → α) ⁻¹' u = Subtype.val ⁻¹' (f '' u) :=
by
ext ⟨b, a, has, rfl⟩
simp [hf.eq_iff]
