closure_eq_right

Mathlib.Combinatorics.Matroid.Closure

URI: https://scilib.ai/kg/mathlib#Matroid.IsBasis.closure_eq_right

English

If I is a basis of cl(X), then cl(I) = cl(X).

Русский

Если I является базисом cl(X), тогда cl(I) = cl(X).

LaTeX

$$$M.IsBasis I (\\operatorname{cl}(X)) \\Rightarrow \\operatorname{cl}(I) = \\operatorname{cl}(X)$$$

Lean4

theorem closure_eq_right (h : M.IsBasis I (M.closure X)) : M.closure I = M.closure X :=
  M.closure_closure X ▸ h.closure_eq_closure

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

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

Разделы

Аффилиация

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