mem_closure_iff — Mathlib

English

For an independent I, an element x belongs to the closure of I exactly when x is dependent when added to I or x already lies in I.

Русский

Для независимого I элемент x принадлежит замыканию I тогда и только тогда, когда I ∪ {x} зависимо или x ∈ I.

LaTeX

$$$x \in \operatorname{cl}(I) \iff \operatorname{Dep}(I \cup \{x\}) \lor x \in I$$$

Lean4

theorem mem_closure_iff (hI : M.Indep I) : x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I := by
  rwa [hI.closure_eq_setOf_isBasis_insert, mem_setOf, isBasis_insert_iff]

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