mem_ground_of_mem_closure

Mathlib.Combinatorics.Matroid.Closure

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

English

If e lies in the closure of X, then e lies in the ground E.

Русский

Если e ∈ cl(X), то e ∈ E.

LaTeX

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

Lean4

@[aesop unsafe 10% (rule_sets := [Matroid])]
theorem mem_ground_of_mem_closure (he : e ∈ M.closure X) : e ∈ M.E :=
  (M.closure_subset_ground _) he

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

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

Разделы

Аффилиация

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