English
Let M be a matroid on α and f: α → β with hf injOn on M.E. Then a pair of subsets (I,X) of β forms a basis of the mapped matroid M.map f hf if and only if there exist I0 and X0 with M.IsBasis I0 X0 and I = f(I0) and X = f(X0).
Русский
Пусть M — матроид над множеством α и f: α → β с инъективным отображением на M.E. Тогда пары подмножеств (I,X) ⊆ β образуют базу в матроиде M.map f hf тогда и только тогда, когда существуют I0, X0 такие, что M.IsBasis I0 X0 и I = f(I0), X = f(X0).
LaTeX
$$$ (M.map f hf).IsBasis I X \iff \exists I_0 X_0, M.IsBasis I_0 X_0 \land I = f(I_0) \land X = f(X_0) $$$
Lean4
theorem map_isBasis_iff' {I X : Set β} {hf} :
(M.map f hf).IsBasis I X ↔ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀ :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· obtain ⟨I, hI, rfl⟩ := subset_image_iff.1 h.indep.subset_ground
obtain ⟨X, hX, rfl⟩ := subset_image_iff.1 h.subset_ground
rw [map_isBasis_iff _ _ hI hX] at h
exact ⟨I, X, h, rfl, rfl⟩
rintro ⟨I, X, hIX, rfl, rfl⟩
exact hIX.map hf
