insert_indep_iff_of_notMem — Mathlib

English

For an independent I and element e, Indep(I ∪ {e}) holds iff e ∈ E \ cl(I).

Русский

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

LaTeX

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

Lean4

theorem insert_indep_iff_of_notMem (hI : M.Indep I) (heI : e ∉ I) : M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I :=
  by
  rw [mem_diff, hI.mem_closure_iff_of_notMem heI, dep_iff, not_and, not_imp_not, insert_subset_iff,
    and_iff_left hI.subset_ground]
  exact ⟨fun h ↦ ⟨h.subset_ground (mem_insert e I), fun _ ↦ h⟩, fun h ↦ h.2 h.1⟩

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