cRk_map_eq — Mathlib

English

Rank under mapping: under an injective map on the ground, the cRk of the mapped matroid equals the cRk of the preimage.

Русский

Ранг под отображением: при инъективном отображении на базу граф ранг отображенного матроида равен рагу прообраза.

LaTeX

$$$(M.map f hf).\\mathrm{cRk} X = M.\\mathrm{cRk}(f^{-1}(X))$$$

Lean4

theorem cRk_map_eq {β : Type u} {f : α → β} {X : Set β} (M : Matroid α) (hf : InjOn f M.E) :
    (M.map f hf).cRk X = M.cRk (f ⁻¹' X) := by
  rw [← M.cRk_inter_ground, ← M.cRk_map_image hf _, image_preimage_inter, ← map_ground _ _ hf, cRk_inter_ground]

Похожие утверждения