exists_insert_of_ssubset — Mathlib

English

If B is a base and I ⊂ B, and B' is a base, then there exists e ∈ B' \\ I such that I ∪ {e} is independent.

Русский

Если B — база, I ⊂ B, и B' — база, то существует e ∈ B' \\ I такое, что I ∪ {e} независимо.

LaTeX

$$M.IsBase(B) ∧ I ⊂ B ∧ M.IsBase(B') ⇒ ∃ e ∈ B' \\ I, M.Indep(I ∪ {e})$$

Lean4

theorem exists_insert_of_ssubset (hB : M.IsBase B) (hIB : I ⊂ B) (hB' : M.IsBase B') :
    ∃ e ∈ B' \ I, M.Indep (insert e I) :=
  (hB.indep.subset hIB.subset).exists_insert_of_not_isBase (fun hI ↦ hIB.ne (hI.eq_of_subset_isBase hB hIB.subset)) hB'

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