map_val_restrictSubtype_ground_eq

English

The restriction M.restrictSubtype M.E, when mapped via the natural inclusion, recovers the original matroid M.

Русский

Ограничение M.restrictSubtype M.E, отображенное через естественное вложение, восстанавливает исходный матроид M.

LaTeX

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

Lean4

/-- `M.restrictSubtype M.E` is isomorphic to `M`. -/
theorem map_val_restrictSubtype_ground_eq (M : Matroid α) :
    (M.restrictSubtype M.E).map (↑) Subtype.val_injective.injOn = M := by simp

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