eq_restrict_removeLoops — Mathlib

English

Restricting the matroid removeLoops(M) to the ground M.E yields M.

Русский

Ограничение матроидa removeLoops(M) к множеству оснований M.E даёт M.

LaTeX

$$$M.removeLoops \restriction M.E = M$$$

Lean4

theorem eq_restrict_removeLoops (M : Matroid α) : M.removeLoops ↾ M.E = M :=
  by
  rw [removeLoops, ext_iff_indep]
  simp only [restrict_ground_eq, restrict_indep_iff, true_and]
  exact fun I hIE ↦ ⟨fun hI ↦ hI.1.1, fun hI ↦ ⟨⟨hI, fun e heI ↦ hI.isNonloop_of_mem heI⟩, hIE⟩⟩

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