notMem_closure_diff_of_mem

Mathlib.Combinatorics.Matroid.Closure

URI: https://scilib.ai/kg/mathlib#Matroid.Indep.notMem_closure_diff_of_mem

English

If I is independent and e ∈ I, then e ∉ closure(I\{e}).

Русский

Если I независимо и e ∈ I, то e ∉ closure(I\{e}).

LaTeX

$$$M.Indep I \land e \in I \Rightarrow e \notin M.closure(I\setminus\{e\})$$$

Lean4

theorem notMem_closure_diff_of_mem (hI : M.Indep I) (he : e ∈ I) : e ∉ M.closure (I \ { e }) :=
  (indep_iff_forall_notMem_closure_diff'.1 hI).2 e he

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

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

Разделы

Аффилиация

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