ofFinitary_finitary — Mathlib

English

The OfFinitary construction yields a finitary matroid structure on matroid.

Русский

Конструкция OfFinitary образует финитную структуру матроида.

LaTeX

$$IndepMatroid.ofFinitary E Indep ... .matroid is Finite$$

Lean4

instance ofFinitary_finitary (E : Set α) (Indep : Set α → Prop) indep_empty indep_subset indep_aug indep_compact
    subset_ground :
    Finitary (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid :=
  ⟨by simpa⟩

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