isBasis_union — Mathlib

English

If I is a basis in X and Y has a basis in I, then I is a basis in X ∪ Y.

Русский

Если I является базисом в X, и Y имеет базис в I, тогда I является базисом X ∪ Y.

LaTeX

$$$ M.IsBasis I X -> M.IsBasis I Y -> M.IsBasis I (X \\cup Y) $$$

Lean4

theorem isBasis_union (hIX : M.IsBasis I X) (hIY : M.IsBasis I Y) : M.IsBasis I (X ∪ Y) := by
  convert hIX.union_isBasis_union hIY _ <;> rw [union_self]; exact hIX.indep

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