English
If f is injective on a preimage of N.E and N.E lies inside range f, then mapping after comap recovers N.
Русский
Если f инъективно действует на предобраз N.E и N.E лежит внутри образа range f, то после применения comap и map получаем N.
LaTeX
$$$ (N.comap\ f).map\ f\ hf = N \,\text{given } h\_range: N.E \subseteq range(f) \text{ and } hf: InjOn f (f^{-1} N.E) $$$
Lean4
theorem map_comap {f : α → β} (h_range : N.E ⊆ range f) (hf : InjOn f (f ⁻¹' N.E)) : (N.comap f).map f hf = N :=
by
refine ext_indep (by simpa [image_preimage_eq_iff]) ?_
simp only [map_ground, comap_ground_eq, map_indep_iff, comap_indep_iff, forall_subset_image_iff]
exact fun I hI ↦ ⟨by grind, fun h ↦ ⟨_, ⟨h, hf.mono hI⟩, rfl⟩⟩
