ofFinite_indep — Mathlib

English

The independence predicate of the finite construction equals the given Indep predicate.

Русский

Аксиомы независимости конечной конструкции совпадают с данным предикатом Indep.

LaTeX

$$$(\\mathrm{IndepMatroid.ofFinite}\\, hE\\, Indep\\, indep\\_empty\\, indep\\_subset\\, indep\\_aug\\, subset\\_ground).Indep = Indep$$$

Lean4

@[simp]
theorem ofFinite_indep {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).Indep = Indep :=
  rfl

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