instRankFiniteMap — Mathlib

English

If a matroid M has finite rank, and f: α → β is injective on the ground set M.E, then the mapped matroid M.map f hf also has finite rank.

Русский

Пусть матроид M имеет конечный ранг, и отображение f: α → β инъективно ограничено на множество оснований M.E. Тогда перенесённый матроид M.map f hf имеет конечный ранг.

LaTeX

$$$[M.RankFinite] \\Rightarrow (M.map f hf).RankFinite$, \\text{ where } hf : Set.InjOn f M.E$$

Lean4

instance [M.RankFinite] {f : α → β} (hf) : (M.map f hf).RankFinite :=
  let ⟨_, hB⟩ := M.exists_isBase
  (hB.map hf).rankFinite_of_finite (hB.finite.image _)

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