ofFinite_E — Mathlib

English

The E-field of IndepMatroid.ofFinite equals E.

Русский

Поле E матроида, построенного методом ofFinite, равно исходному E.

LaTeX

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

Lean4

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

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