insert_isBase_of_insert_indep — Mathlib

English

Let I be a set, and e, f elements not in I. If I ∪ {e} is a base of M and I ∪ {f} is independent, then I ∪ {f} is a base of M.

Русский

Пусть I — множество; элементы e, f не принадлежат I. Если I ∪ {e} является базой матроида M и I ∪ {f} независимо, то I ∪ {f} является базой.

LaTeX

$$$e \\notin I \\land f \\notin I \\land M.IsBase(I \\cup \\{e\\}) \\land M.Indep(I \\cup \\{f\\}) \\Rightarrow M.IsBase(I \\cup \\{f\\})$$$

Lean4

theorem insert_isBase_of_insert_indep {M : Matroid α} {I : Set α} {e f : α} (he : e ∉ I) (hf : f ∉ I)
    (heI : M.IsBase (insert e I)) (hfI : M.Indep (insert f I)) : M.IsBase (insert f I) :=
  by
  obtain rfl | hef := eq_or_ne e f
  · assumption
  simpa [diff_singleton_eq_self he, hfI] using heI.exchange_isBase_of_indep (e := e) (f := f) (by simp [hef.symm, hf])

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