antisymm

Mathlib.Combinatorics.Matroid.Minor.Restrict

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

English

If M ≤r M' and M' ≤r M, then M = M'.

Русский

Если M ≤r M' и M' ≤r M, то M = M'.

LaTeX

$$$ M \\le_r M' \\land M' \\le_r M \\Rightarrow M = M' $$$

Lean4

theorem antisymm {M' : Matroid α} (h : M ≤r M') (h' : M' ≤r M) : M = M' := by
  simpa using (ofMatroid_le_iff.2 h).antisymm (ofMatroid_le_iff.2 h')

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

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

Разделы

Аффилиация

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