isStrictMinor_iff_isMinor_ne

Mathlib.Combinatorics.Matroid.Minor.Order

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

English

A matroid N is a strict minor of M iff N is a minor of M and N ≠ M.

Русский

Матроид N является строгим минором M тогда и только тогда, когда N является минором M и N ≠ M.

LaTeX

$$N

Lean4

theorem isStrictMinor_iff_isMinor_ne : N <m M ↔ N ≤m M ∧ N ≠ M :=
  lt_iff_le_and_ne (α := Matroid α)

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

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

Разделы

Аффилиация

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