English
Under a base-preserving map f, (M.map f hf).IsBasis (f''I) (f''X) is equivalent to M.IsBasis I X, provided I,X ⊆ M.E.
Русский
При отображении, сохраняющем базис, (M.map f hf).IsBasis (f''I) (f''X) эквивалентно M.IsBasis I X при условии I,X ⊆ M.E.
LaTeX
$$$(M.map f hf).IsBasis (f''I) (f''X) \iff M.IsBasis I X \quad (I,X \subseteq M.E)$$$
Lean4
theorem map_isBasis_iff {I X : Set α} (f : α → β) (hf) (hI : I ⊆ M.E) (hX : X ⊆ M.E) :
(M.map f hf).IsBasis (f '' I) (f '' X) ↔ M.IsBasis I X :=
by
refine ⟨fun h ↦ ?_, fun h ↦ h.map hf⟩
obtain ⟨I', hI', hII'⟩ := map_indep_iff.1 h.indep
rw [hf.image_eq_image_iff hI hI'.subset_ground] at hII'
obtain rfl := hII'
have hss := (hf.image_subset_image_iff hI hX).1 h.subset
refine hI'.isBasis_of_maximal_subset hss (fun J hJ hIJ hJX ↦ ?_)
have hIJ' := h.eq_of_subset_indep (hJ.map f hf) (image_mono hIJ) (image_mono hJX)
rw [hf.image_eq_image_iff hI hJ.subset_ground] at hIJ'
exact hIJ'.symm.subset
