instRankPosMap — Mathlib

English

If a matroid M has positive rank (RankPos), and f : α → β is injective on M.E, then M.map f hf has RankPos.

Русский

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

LaTeX

$$$[M.RankPos] \\Rightarrow (M.map f hf).RankPos$, \\text{ где } hf : Set.InjOn f M.E$$

Lean4

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

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