restrict_univ_removeLoops_eq — Mathlib

English

Restricting the removeLoops of M to univ is the same as removing loops from M.

Русский

Ограничение M.removeLoops до единицы совпадает с removeLoops(M).

LaTeX

$$$\operatorname{restrict}_{\operatorname{univ}}(M).removeLoops = M.removeLoops$$$

Lean4

@[simp]
theorem restrict_univ_removeLoops_eq : (M ↾ univ).removeLoops = M.removeLoops :=
  by
  rw [removeLoops_eq_restrict, restrict_restrict_eq _ (subset_univ _), removeLoops_eq_restrict]
  simp

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