comap_indep_iff_of_injOn — Mathlib

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

Похожие утверждения