eRk_comap — Mathlib

English

The loopy construction has zero eRk: eRk(loopyOn Y) X = 0.

Русский

У конструкции loopyOn имеет нулевой eRk: eRk(loopyOn Y) X = 0.

LaTeX

$$$(loopyOn Y).eRk X = 0$$$

Lean4

@[simp]
theorem eRk_comap {β : Type*} {f : α → β} (M : Matroid β) (X : Set α) : (M.comap f).eRk X = M.eRk (f '' X) :=
  by
  obtain ⟨I, hI⟩ := (M.comap f).exists_isBasis' X
  obtain ⟨hI', hinj, -⟩ := comap_isBasis'_iff.1 hI
  rw [← hI.encard_eq_eRk, ← hI'.encard_eq_eRk, hinj.encard_image]

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