antisymm

Mathlib.Combinatorics.Matroid.Minor.Order

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

English

If N is a minor of M and M is a minor of N, then N and M are equal.

Русский

Если N является минором M и M является минором N, то N равно M.

LaTeX

$$$(N \le_m M) \land (M \le_m N) \Rightarrow N = M$$$

Lean4

theorem antisymm (h : N ≤m M) (h' : M ≤m N) : N = M :=
  h'.eq_of_ground_subset h.subset

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

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

Разделы

Аффилиация

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