mem_closure_iff_of_notMem — Mathlib

English

If I is independent and e ∉ I, then e ∈ cl(I) iff I ∪ {e} is dependent.

Русский

Если I независим и e ∉ I, то e ∈ cl(I) тогда и только тогда, когда I ∪ {e} зависимо.

LaTeX

$$$e \in I^c \Rightarrow (e \in \operatorname{cl}(I) \iff \operatorname{Dep}(I \cup \{e\}))$$$

Lean4

theorem mem_closure_iff_of_notMem (hI : M.Indep I) (heI : e ∉ I) : e ∈ M.closure I ↔ M.Dep (insert e I) := by
  rw [hI.insert_dep_iff, mem_diff, and_iff_left heI]

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