closure_eq_closure

Mathlib.Combinatorics.Matroid.Closure

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

← MathLib Explorer

English

For IsBasis' I X, closure of I equals closure of X.

Русский

Для IsBasis' I X: closure I = closure X.

LaTeX

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

Lean4

theorem closure_eq_closure (h : M.IsBasis' I X) : M.closure I = M.closure X := by
  rw [← closure_inter_ground _ X, h.isBasis_inter_ground.closure_eq_closure]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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