eRank_map — Mathlib

English

Comap preserves rank up to image: (M.comap f).eRk X = M.eRk (f '' X).

Русский

Комап сохраняет ранг вплоть до образа: (M.comap f).eRk X = M.eRk (f '' X).

LaTeX

$$$ (M.comap f).eRk X = M.eRk (f''X) $$$

Lean4

@[simp]
theorem eRank_map {β : Type*} {f : α → β} (M : Matroid α) (hf : InjOn f M.E) : (M.map f hf).eRank = M.eRank :=
  by
  obtain ⟨B, hB⟩ := M.exists_isBase
  rw [← (hB.map hf).encard_eq_eRank, ← hB.encard_eq_eRank, (hf.mono hB.subset_ground).encard_image]

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