insert_dep_iff — Mathlib

English

For an independent I and an element e, Dep(I ∪ {e}) holds exactly when e ∈ cl(I) \ I.

Русский

Для независимого I и элемента e выполняется Dep(I ∪ {e}) тогда и только тогда, когда e ∈ cl(I) \ I.

LaTeX

$$$\operatorname{Dep}(I \cup \{e\}) \iff e \in \operatorname{cl}(I) \setminus I$$$

Lean4

theorem insert_dep_iff (hI : M.Indep I) : M.Dep (insert e I) ↔ e ∈ M.closure I \ I :=
  by
  rw [mem_diff, hI.mem_closure_iff, or_and_right, and_not_self_iff, or_false, iff_self_and, imp_not_comm]
  intro heI; rw [insert_eq_of_mem heI]; exact hI.not_dep

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