comap_rankFinite — Mathlib

English

If N has finite rank, then its comap by f also has finite rank.

Русский

Если у N конечная ранг, то и у N comap по f конечный ранг.

LaTeX

$$N.RankFinite \Rightarrow (N.comap f).RankFinite$$

Lean4

instance comap_rankFinite (N : Matroid β) [N.RankFinite] (f : α → β) : (N.comap f).RankFinite :=
  by
  obtain ⟨B, hB⟩ := (N.comap f).exists_isBase
  refine hB.rankFinite_of_finite ?_
  simp only [comap_isBase_iff] at hB
  exact (hB.1.indep.finite.of_finite_image hB.2.1)

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