ofFinitaryCardAugment_indep — Mathlib

English

Equality of Indep under OfFinitaryCardAugment: the Indep predicate matches the generated matroid's Indep.

Русский

Согласованность Indep при OfFinitaryCardAugment: предикат Indep совпадает с Indep сгенерированного матроида.

LaTeX

$$IndepMatroid.ofFinitaryCardAugment ... .Indep = Indep$$

Lean4

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

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