eRk_eq_eRk_of_subset_of_le

Mathlib.Combinatorics.Matroid.Rank.ENat

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

English

If X ⊆ Y and eRk(Y) ≤ eRk(X) then eRk(X) = eRk(Y).

Русский

Если X ⊆ Y и eRk(Y) ≤ eRk(X), то eRk(X) = eRk(Y).

LaTeX

$$$ (X \\subseteq Y) \\land (M.eRk(Y) \\le M.eRk(X)) \\Rightarrow M.eRk(X) = M.eRk(Y) $$$

Lean4

theorem eRk_eq_eRk_of_subset_of_le (hXY : X ⊆ Y) (hYX : M.eRk Y ≤ M.eRk X) : M.eRk X = M.eRk Y :=
  (M.eRk_mono hXY).antisymm hYX

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

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

Разделы

Аффилиация

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