comap_isBasis'_iff — Mathlib

English

IsBasis' for comap is equivalent to IsBasis' on the image and preimage data with injOn and subset conditions.

Русский

IsBasis' для comap эквивалентно IsBasis' на образе и подмножестве с условиями injOn.

LaTeX

$$(N.comap f).IsBasis' I X \iff N.IsBasis' (f '' I) (f '' X) ∧ I.InjOn f ∧ I ⊆ X$$

Lean4

@[simp]
theorem comap_isBasis'_iff {I X : Set α} :
    (N.comap f).IsBasis' I X ↔ N.IsBasis' (f '' I) (f '' X) ∧ I.InjOn f ∧ I ⊆ X :=
  by
  simp only [isBasis'_iff_isBasis_inter_ground, comap_ground_eq, comap_isBasis_iff, image_inter_preimage,
    subset_inter_iff, ← and_assoc, and_iff_left_iff_imp, and_imp]
  exact fun h _ _ ↦ (image_subset_iff.1 h.indep.subset_ground)

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