uniqueBaseOn — Mathlib

English

The matroid uniqueBaseOn(I,E) is defined as the restriction of freeOn I to E.

Русский

Матроид uniqueBaseOn(I,E) определяется как ограничение freeOn I к E.

LaTeX

$$$ uniqueBaseOn(I,E) := freeOn(I) \restriction E $$$

Lean4

/-- The matroid on `E` whose unique base is the subset `I` of `E`.
Intended for use when `I ⊆ E`; if this is not the case, then the base is `I ∩ E`. -/
def uniqueBaseOn (I E : Set α) : Matroid α :=
  freeOn I ↾ E

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