English
If I is a basis of X in M (I ⊆ X ⊆ M.E), then under any embedding f, the image (f''I, f''X) forms a basis of M.mapEmbedding f.
Русский
Если I является базисом множества X в M (I ⊆ X ⊆ M.E), то под отображением f образ (f''I, f''X) образует базис у M.mapEmbedding f.
LaTeX
$$$M.IsBasis\; I\; X \Rightarrow (M.mapEmbedding f hf).IsBasis\; (f''I)\; (f''X)$$$
Lean4
theorem map {X : Set α} (hIX : M.IsBasis I X) {f : α → β} (hf) : (M.map f hf).IsBasis (f '' I) (f '' X) :=
by
refine (hIX.indep.map f hf).isBasis_of_forall_insert (image_mono hIX.subset) ?_
rintro _ ⟨⟨e, he, rfl⟩, he'⟩
have hss := insert_subset (hIX.subset_ground he) hIX.indep.subset_ground
rw [← not_indep_iff (by simpa [← image_insert_eq] using image_mono hss)]
simp only [map_indep_iff, not_exists, not_and]
intro J hJ hins
rw [← image_insert_eq, hf.image_eq_image_iff hss hJ.subset_ground] at hins
obtain rfl := hins
exact he' (mem_image_of_mem f (hIX.mem_of_insert_indep he hJ))
