subset_closure_diff_singleton

Mathlib.Combinatorics.Matroid.Circuit

URI: https://scilib.ai/kg/mathlib#Matroid.IsCircuit.subset_closure_diff_singleton

← MathLib Explorer

English

If C is a circuit, then C is contained in the closure of C \\ {e}.

Русский

Если C является окружностью, то C ⊆ closure( C \\ {e} ).

LaTeX

$$$\\forall {\\alpha} {M : Matroid \\alpha} {C}, M.IsCircuit C \\to C \\subseteq M.closure (C \\ { e })$$$

Lean4

theorem subset_closure_diff_singleton (hC : M.IsCircuit C) (e : α) : C ⊆ M.closure (C \ { e }) :=
  by
  rw [hC.closure_diff_singleton_eq]
  exact M.subset_closure _ hC.subset_ground

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

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

Разделы

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

Аффилиация

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