instRankFiniteMatroidOfBdd — Mathlib

English

The matroid produced by OfBdd is RankFinite when the independence predicate is bounded.

Русский

Матроид, полученный с помощью OfBdd, имеет свойство RankFinite при наличии границы рангa.

LaTeX

$$∀ {E} {Indep} ..., (IndepMatroid.ofBdd E Indep ...).matroid.RankFinite$$

Lean4

/-- `IndepMatroid.ofBdd` constructs a `RankFinite` matroid. -/
instance (E : Set α) (Indep : Set α → Prop) indep_empty indep_subset indep_aug subset_ground h_bdd :
    RankFinite (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid :=
  by
  obtain ⟨B, hB⟩ := (IndepMatroid.ofBdd E Indep _ _ _ _ _).matroid.exists_isBase
  refine hB.rankFinite_of_finite ?_
  obtain ⟨n, hn⟩ := h_bdd
  exact finite_of_encard_le_coe <| hn B (by simpa using hB.indep)

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