insert_indep_of_indep — Mathlib

English

If e is a Coloop and I is independent, then I ∪ {e} is independent.

Русский

Если e — колооп, а I — независимое множество, то I ∪ {e} — независимое.

LaTeX

$$$$ M.IsColoop(e) \wedge M.Indep(I) \Rightarrow M.Indep(I \cup \{e\}). $$$$

Lean4

theorem insert_indep_of_indep (he : M.IsColoop e) (hI : M.Indep I) : M.Indep (insert e I) :=
  by
  refine (em (e ∈ I)).elim (fun h ↦ by rwa [insert_eq_of_mem h]) fun h ↦ ?_
  rw [← hI.notMem_closure_iff_of_notMem h]
  exact he.notMem_closure_of_notMem h

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