English
The dual of the mapped matroid equals the mapped dual matroid. Specifically, (M.map f hf)✶ = M✶.map f hf.
Русский
Дуал матроида, полученного после отображения, равен отображённому дуалу исходного матроида: (M.map f hf)✶ = M✶.map f hf.
LaTeX
$$$ (M.map f hf)^{\ast} = M^{\ast}.map f hf $$$
Lean4
@[simp]
theorem map_dual {hf} : (M.map f hf)✶ = M✶.map f hf :=
by
apply ext_isBase (by simp)
simp only [dual_ground, map_ground, subset_image_iff, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
dual_isBase_iff']
intro B hB
simp_rw [← hf.image_diff_subset hB, map_image_isBase_iff diff_subset, map_image_isBase_iff (show B ⊆ M✶.E from hB),
dual_isBase_iff hB, and_iff_left_iff_imp]
exact fun _ ↦ ⟨B, hB, rfl⟩
