restrict_isStrictRestriction — Mathlib

English

If R is a proper subset of the ground set M.E, then the restriction M|_R is a strict restriction of M.

Русский

Если R ⊂ M.E, то ограничение M|_R является строгое ограничение M.

LaTeX

$$$ M|_R <_r M $$$

Lean4

theorem restrict_isStrictRestriction {M : Matroid α} (hR : R ⊂ M.E) : M ↾ R <r M :=
  by
  refine (M.restrict_isRestriction R hR.subset).isStrictRestriction_of_ne (fun h ↦ ?_)
  rw [← h, restrict_ground_eq] at hR
  exact hR.ne rfl

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