isStrictRestriction_of_ground_ne

Mathlib.Combinatorics.Matroid.Minor.Restrict

URI: https://scilib.ai/kg/mathlib#Matroid.IsRestriction.isStrictRestriction_of_ground_ne

← MathLib Explorer

English

If N ≤r M and N.E ≠ M.E, then N <r M.

Русский

Если N ≤r M и N.E ≠ M.E, тогда N <r M.

LaTeX

$$$ N <_r M $$$

Lean4

theorem isStrictRestriction_of_ground_ne (h : N ≤r M) (hne : N.E ≠ M.E) : N <r M :=
  by
  rw [← h.eq_restrict]
  exact restrict_isStrictRestriction (h.subset.ssubset_of_ne hne)

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

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

Разделы

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

Аффилиация

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