cRk_closure_congr

Mathlib.Combinatorics.Matroid.Rank.Cardinal

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

English

If M.closure X = M.closure Y, then cRk X = cRk Y.

Русский

Если M.closure(X) = M.closure(Y), то cRk(X) = cRk(Y).

LaTeX

$$$M.cRk(X) = M.cRk(Y)$ given $M.closure X = M.closure Y$$$

Lean4

theorem cRk_closure_congr (hXY : M.closure X = M.closure Y) : M.cRk X = M.cRk Y := by
  rw [← cRk_closure, hXY, cRk_closure]

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

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

Разделы

Аффилиация

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