English
A subset D of β is dependent in the mapped matroid M.map f hf if and only if there exists a subset D0 of α with D0 dependent in M and D = f''D0.
Русский
Подмножество D ⊆ β является зависимым в отображённом матроидe M.map f hf тогда и только тогда существует подмножество D0 ⊆ α, зависящее в M, и D = f''D0.
LaTeX
$$$(M.map f\; hf).Dep\; D \;\iff\; \exists D_0,\; M.Dep\; D_0 \land D = f''D_0$$$
Lean4
theorem map_dep_iff {hf} {D : Set β} : (M.map f hf).Dep D ↔ ∃ D₀, M.Dep D₀ ∧ D = f '' D₀ :=
by
simp only [Dep, map_indep_iff, not_exists, not_and, map_ground, subset_image_iff]
constructor
· rintro ⟨h, D₀, hD₀E, rfl⟩
exact ⟨D₀, ⟨fun hd ↦ h _ hd rfl, hD₀E⟩, rfl⟩
rintro ⟨D₀, ⟨hD₀, hD₀E⟩, rfl⟩
refine ⟨fun I hI h_eq ↦ ?_, ⟨_, hD₀E, rfl⟩⟩
rw [hf.image_eq_image_iff hD₀E hI.subset_ground] at h_eq
subst h_eq; contradiction
