ofIsBaseOfFinite_isBase — Mathlib

English

The IsBase field of Matroid.ofIsBaseOfFinite equals the base predicate.

Русский

Поле IsBase у Matroid.ofIsBaseOfFinite равно IsBase.

LaTeX

$$$(Matroid.ofIsBaseOfFinite\\ hE\\ IsBase\\ exists_isBase\\ isBase_exchange\\ subset_ground).IsBase = IsBase$$$

Lean4

@[simp]
theorem ofIsBaseOfFinite_isBase {E : Set α} (hE : E.Finite) IsBase exists_isBase isBase_exchange subset_ground :
    (Matroid.ofIsBaseOfFinite hE IsBase exists_isBase isBase_exchange subset_ground).IsBase = IsBase :=
  rfl

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