ofFinitary_indep — Mathlib

English

In the OfFinitary construction, the resulting matroid's independence predicate equals the given Indep.

Русский

В конструировании OfFinitary у полученного матроида независимость совпадает с заданным предикатом Indep.

LaTeX

$$(IndepMatroid.ofFinitary E Indep ...).Indep = Indep$$

Lean4

@[simp]
theorem ofFinitary_indep (E : Set α) (Indep : Set α → Prop) indep_empty indep_subset indep_aug indep_compact
    subset_ground :
    (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).Indep = Indep :=
  rfl

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