restrictSubtype_isBasis_iff — Mathlib

English

IsBasis for the restriction to Y corresponds to IsBasis' on M.

Русский

IsBasis для ограничения на Y эквивалентно IsBasis' для M.

LaTeX

$$$(M.restrictSubtype Y).IsBasis I X \iff M.IsBasis' I X$$$

Lean4

theorem restrictSubtype_isBasis_iff {Y : Set α} {I X : Set Y} : (M.restrictSubtype Y).IsBasis I X ↔ M.IsBasis' I X :=
  by
  rw [restrictSubtype, comap_isBasis_iff, and_iff_right Subtype.val_injective.injOn, and_iff_left_of_imp,
    isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground]
  · simp
  exact fun h ↦ (image_subset_image_iff Subtype.val_injective).1 h.subset

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