union_isBasis_union — Mathlib

English

If I is a basis of X and J is a basis of Y, then I ∪ J is a basis of X ∪ Y, provided I and J are compatible in independence.

Русский

Если I является базисом X, а J — базисом Y, тогда I ∪ J является базисом X ∪ Y, при условии независимости I ∪ J.

LaTeX

$$$ M.IsBasis I X \\rightarrow M.IsBasis J Y \\rightarrow M.IsBasis (I \\cup J) (X \\cup Y) $$$

Lean4

theorem union_isBasis_union (hIX : M.IsBasis I X) (hJY : M.IsBasis J Y) (h : M.Indep (I ∪ J)) :
    M.IsBasis (I ∪ J) (X ∪ Y) := by
  rw [union_eq_iUnion, union_eq_iUnion]
  refine IsBasis.iUnion_isBasis_iUnion _ _ ?_ ?_
  · simp only [Bool.forall_bool, cond_false, cond_true]; exact ⟨hJY, hIX⟩
  rwa [← union_eq_iUnion]

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