English
If M has invariant cardinal rank, then M.comap f has invariant cardinal rank.
Русский
Если у M инвариантная кардинальная ранга, то M.comap f имеет инвариантную кардинальную ранг.
LaTeX
$$InvariantCardinalRank (M.comap f)$$
Lean4
instance invariantCardinalRank_comap (M : Matroid β) [InvariantCardinalRank M] (f : α → β) :
InvariantCardinalRank (M.comap f) := by
refine ⟨fun I J X hI hJ ↦ ?_⟩
obtain ⟨hI, hfI, hIX⟩ := comap_isBasis_iff.1 hI
obtain ⟨hJ, hfJ, hJX⟩ := comap_isBasis_iff.1 hJ
rw [← lift_inj.{u, v}, ← mk_image_eq_of_injOn_lift _ _ (hfI.mono diff_subset), ←
mk_image_eq_of_injOn_lift _ _ (hfJ.mono diff_subset), lift_inj, hfI.image_diff, hfJ.image_diff, ←
diff_union_diff_cancel inter_subset_left (image_inter_subset f I J), inter_comm, diff_inter_self_eq_diff,
mk_union_of_disjoint, hI.cardinalMk_diff_comm hJ, ←
diff_union_diff_cancel inter_subset_left (image_inter_subset f J I), inter_comm, diff_inter_self_eq_diff,
mk_union_of_disjoint, inter_comm J I] <;>
exact disjoint_sdiff_left.mono_right (diff_subset.trans inter_subset_left)
