restrict — Mathlib

English

If N is a strict minor of M, then N.E ⊂ M.E.

Русский

Если N является строгим минором M, то N.E ⊂ M.E.

LaTeX

$$N.E \subset M.E$$

Lean4

/-- Change the ground set of a matroid to some `R : Set α`. The independent sets of the restriction
are the independent subsets of the new ground set. Most commonly used when `R ⊆ M.E`,
but it is convenient not to require this. The elements of `R \ M.E` become 'loops'. -/
def restrict (M : Matroid α) (R : Set α) : Matroid α :=
  (M.restrictIndepMatroid R).matroid

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