removeLoops_eq_self_iff

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.removeLoops_eq_self_iff

← MathLib Explorer

English

The equality removeLoops(M) = M holds if and only if M is loopless.

Русский

Равенство removeLoops(M) = M выполняется тогда, если и только если M не имеет петель.

LaTeX

$$$\operatorname{removeLoops}(M) = M \iff \text{Loopless}(M)$$$

Lean4

theorem removeLoops_eq_self_iff : M.removeLoops = M ↔ M.Loopless :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ M.removeLoops_eq_self⟩
  rw [← h]
  infer_instance

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

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

Разделы

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

Аффилиация

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