restrict_idem — Mathlib

English

Let M be a matroid on a set α and R ⊆ α. Restricting M to R and then restricting again to R yields the same matroid as restricting once: (M|R)|R = M|R.

Русский

Пусть M — матроид на множестве α и R ⊆ α. Ограничение M до R с последующим повторным ограничением до R совпадает с ограничением M до R один раз: (M|R)|R = M|R.

LaTeX

$$$ (M|R)|R = M|R $$$

Lean4

@[simp]
theorem restrict_idem (M : Matroid α) (R : Set α) : M ↾ R ↾ R = M ↾ R := by rw [M.restrict_restrict_eq Subset.rfl]

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