notMem_of_mem_diff_closure

Mathlib.Combinatorics.Matroid.Closure

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

English

If e belongs to the ground E but not to the closure of X, then e does not belong to X.

Русский

Если e ∈ E \\operatorname{cl}(X), тогда e ∉ X.

LaTeX

$$$e \\in M.E \\setminus \\operatorname{cl}(X) \\Rightarrow e \\notin X$$$

Lean4

theorem notMem_of_mem_diff_closure (he : e ∈ M.E \ M.closure X) : e ∉ X := fun heX ↦
  he.2 <| M.mem_closure_of_mem' heX he.1

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

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

Разделы

Аффилиация

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