English
If f is InjOn on f^{-1}(N.E), then independence in the pullback equates to independence of the image.
Русский
Если f инъективна на f^{-1}(N.E), независимость в проекции обратно эквивалентна независимости образа.
LaTeX
$$(hf : InjOn f (f^{-1} N.E)) : (N.comap f).Indep I \iff N.Indep (f '' I)$$
Lean4
theorem comap_indep_iff_of_injOn (hf : InjOn f (f ⁻¹' N.E)) : (N.comap f).Indep I ↔ N.Indep (f '' I) :=
by
rw [comap_indep_iff, and_iff_left_iff_imp]
refine fun hi ↦ hf.mono <| subset_trans ?_ (preimage_mono hi.subset_ground)
apply subset_preimage_image