map_val_restrictSubtype_eq — Mathlib

English

The matroid obtained from restricting M to X, when mapped along the natural inclusion into the ambient ground set, coincides with the usual restriction of M to X.

Русский

Матроид, полученный при ограничении M до X, при отображении по естественному вложению в исходное множество совпадает с обычным ограничением M до X.

LaTeX

$$$ (M\\restrictSubtype X).map(\\uparrow)\\,\\mathrm{injOn} = M \\restriction X $$$

Lean4

/-- `M.restrictSubtype X` is isomorphic to `M ↾ X`. -/
@[simp]
theorem map_val_restrictSubtype_eq (M : Matroid α) (X : Set α) :
    (M.restrictSubtype X).map (↑) Subtype.val_injective.injOn = M ↾ X := by simp [restrictSubtype, map_comap]

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