English
For an embedding f, the IsBasis property transfers exactly via preimages and images with the appropriate subset relations.
Русский
Для вложения f свойство IsBasis передается точно через предобраз и образ с соответсвующими отношениями подмножества.
LaTeX
$$$(M.mapEmbedding f).IsBasis I X \\iff M.IsBasis (f^{-1}' I) (f^{-1}' X) \\wedge (I \\subseteq X) \\wedge (X \\subseteq \\operatorname{range} f)$$$
Lean4
@[simp]
theorem mapEmbedding_isBasis_iff {f : α ↪ β} {I X : Set β} :
(M.mapEmbedding f).IsBasis I X ↔ M.IsBasis (f ⁻¹' I) (f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range f :=
by
rw [mapEmbedding, map_isBasis_iff']
refine ⟨?_, fun ⟨hb, hIX, hX⟩ ↦ ?_⟩
· rintro ⟨I, X, hIX, rfl, rfl⟩
simp [preimage_image_eq _ f.injective, image_mono hIX.subset, hIX]
obtain ⟨X, rfl⟩ := subset_range_iff_exists_image_eq.1 hX
obtain ⟨I, -, rfl⟩ := subset_image_iff.1 hIX
exact ⟨I, X, by simpa [preimage_image_eq _ f.injective] using hb⟩
