ofFinite_finite — Mathlib · SciLib

English

A construction from a finite base set yields a matroid whose ground is the given finite set.

Русский

Конструкция, заданная конечной базой, порождает матроид, опорное множество которого равно заданному конечному множеству.

LaTeX

$$$\\mathrm{IndepMatroid.ofFinite}\\dots .matroid.Finite$$$

Lean4

instance ofFinite_finite {E : Set α} hE Indep indep_empty indep_subset indep_aug subset_ground :
    (IndepMatroid.ofFinite (hE : E.Finite) Indep indep_empty indep_subset indep_aug subset_ground).matroid.Finite :=
  ⟨hE⟩

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