English
For any subset s of the target, the image I''s equals the intersection of the inverse image I.symm⁻¹(s) with the range of I; equivalently, I''s = { y ∈ range(I) : I^{-1}(y) ∈ s }.
Русский
Для любого множества s образ I''s совпадает с пересечением обратного образа I.symm⁻¹(s) и множества range(I); эквивалентно: I''s = { y ∈ range(I) : I^{-1}(y) ∈ s }.
LaTeX
$$$I''s = \\{ y \\in \\operatorname{range}(I) \mid I^{-1}(y) \\in s \\} = (\\operatorname{range}(I)) \\cap I^{-1}(s)$$$
Lean4
protected theorem image_eq (s : Set H) : I '' s = I.symm ⁻¹' s ∩ range I :=
by
refine (I.toPartialEquiv.image_eq_target_inter_inv_preimage ?_).trans ?_
· rw [I.source_eq]; exact subset_univ _
· rw [inter_comm, I.target_eq, I.toPartialEquiv_coe_symm]
