isNonloop_iff_delete_of_notMem

Mathlib.Combinatorics.Matroid.Minor.Delete

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

← MathLib Explorer

English

If e ∉ D, then M.IsNonloop e iff (M \ D).IsNonloop e.

Русский

Если e не принадлежит D, то M.IsNonloop e эквивалентно (M \ D).IsNonloop e.

LaTeX

$$$ e \notin D \Rightarrow (M.IsNonloop(e) \iff (M \setminus D).IsNonloop(e)) $$$

Lean4

theorem isNonloop_iff_delete_of_notMem (he : e ∉ D) : M.IsNonloop e ↔ (M ＼ D).IsNonloop e :=
  ⟨fun h ↦ delete_isNonloop_iff.2 ⟨h, he⟩, fun h ↦ h.of_delete⟩

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

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

Разделы

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

Аффилиация

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