isStrictMinor_iff_isMinor_ssubset

Mathlib.Combinatorics.Matroid.Minor.Order

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

← MathLib Explorer

English

A minor N is strict of M iff N is a minor of M and N.E ⊂ M.E.

Русский

Строгий минор N от M эквивалентен тому, что N является минором M и N.E ⊂ M.E.

LaTeX

$$N

Lean4

theorem isStrictMinor_iff_isMinor_ssubset : N <m M ↔ N ≤m M ∧ N.E ⊂ M.E :=
  ⟨fun h ↦ ⟨h.isMinor, h.ssubset⟩, fun ⟨h, hss⟩ ↦ ⟨h, fun h' ↦ hss.ne <| by rw [h'.antisymm h]⟩⟩

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

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

Разделы

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

Аффилиация

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