isRestriction_removeLoops

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsRestriction.isRestriction_removeLoops

← MathLib Explorer

English

If N ≤r M, then N.removeLoops ≤r M.removeLoops.

Русский

Если N ≤r M, то N.removeLoops ≤r M.removeLoops.

LaTeX

$$$N \le_r M \Rightarrow N.removeLoops \le_r M.removeLoops$$$

Lean4

theorem isRestriction_removeLoops (hNM : N ≤r M) [N.Loopless] : N ≤r M.removeLoops :=
  by
  obtain ⟨R, hR, rfl⟩ := hNM.exists_eq_restrict
  exact IsRestriction.of_subset M fun e heR ↦ ((M ↾ R).isNonloop_of_loopless heR).of_restrict

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru