of_isMinor

Mathlib.Combinatorics.Matroid.Minor.Order

URI: https://scilib.ai/kg/mathlib#Matroid.IsNonloop.of_isMinor

Lean4

theorem of_isMinor (h : N.IsNonloop e) (hNM : N ≤m M) : M.IsNonloop e :=
  by
  obtain ⟨C, D, rfl⟩ := hNM
  exact h.of_delete.of_contract

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

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

Разделы

Аффилиация

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