notMem_closure_of_notMem

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsColoop.notMem_closure_of_notMem

English

If e is a Coloops in M, and e is not in X, then e is not in the closure of X: e ∉ M.closure(X).

Русский

Если e является колоопом в M и e ∉ X, то e не принадлежит замыканию X.

LaTeX

$$$$ M.IsColoop(e) \land e \notin X \Rightarrow e \notin \operatorname{cl}_M(X). $$$$

Lean4

theorem notMem_closure_of_notMem (he : M.IsColoop e) (hX : e ∉ X) : e ∉ M.closure X :=
  mt he.mem_closure_iff_mem.mp hX

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

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

Разделы

Аффилиация

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