exists_isBase_subset_union_isBase

English

If I is independent and B is a base, there exists B' with B' a base, I ⊆ B' ⊆ I ∪ B.

Русский

Если I независимо, и B является базисом, существует B' такой, что B' — базис, I ⊆ B' ⊆ I ∪ B.

LaTeX

$$$ M.Indep I \\rightarrow M.IsBase B \\rightarrow \\exists B'\\, (M.IsBase B') \\land (I \\subseteq B') \\land (B' \\subseteq I \\cup B) $$$

Lean4

theorem exists_isBase_subset_union_isBase (hI : M.Indep I) (hB : M.IsBase B) :
    ∃ B', M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B :=
  by
  obtain ⟨B', hB', hIB'⟩ := hI.subset_isBasis_of_subset <| subset_union_left (t := B)
  exact ⟨B', hB.isBase_of_isBasis_superset subset_union_right hB', hIB', hB'.subset⟩

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