insert_indep_iff — Mathlib

English

For any I and e, Indep(I ∪ {e}) is equivalent to e ∈ E \ cl(I) or e ∈ I.

Русский

Для любых I и e, Indep(I ∪ {e}) эквивалентно e ∈ E \ cl(I) или e ∈ I.

LaTeX

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

Lean4

theorem insert_indep_iff : M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I) :=
  by
  by_cases hI : M.Indep I
  · rw [hI.insert_indep_iff, and_iff_right hI, or_iff_not_imp_right]
  simp [hI, show ¬M.Indep (insert e I) from fun h ↦ hI <| h.subset <| subset_insert _ _]

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