delete_closure_eq_of_disjoint

Mathlib.Combinatorics.Matroid.Minor.Delete

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

← MathLib Explorer

English

If X and D are disjoint, then (M \ D).closure X = M.closure X \ D.

Русский

Если X и D дизjointы, то (M \ D).closure X = M.closure X \ D.

LaTeX

$$$ Disjoint(X,D) \Rightarrow (M \setminus D).closure(X) = M.closure(X) \setminus D $$$

Lean4

theorem delete_closure_eq_of_disjoint (M : Matroid α) {D X : Set α} (hXD : Disjoint X D) :
    (M ＼ D).closure X = M.closure X \ D := by rw [delete_closure_eq, hXD.sdiff_eq_left]

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

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

Разделы

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

Аффилиация

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