ofFinset_E — Mathlib · SciLib

English

For Finset-based independence, the E-set is the ground of the resulting matroid on α.

Русский

Для независимости на Finset E задаёт опорное множество матроида на α.

LaTeX

$$$\\mathrm{ofFinset\\_E}\\; E\\; Indep\\; indep\\_empty\\; indep\\_subset\\; indep\\_aug\\; subset\\_ground:\\; E = E$$$

Lean4

@[simp]
theorem ofFinset_E [DecidableEq α] (E : Set α) Indep indep_empty indep_subset indep_aug subset_ground :
    (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).E = E :=
  rfl

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