isBasis_iUnion — Mathlib

English

If I is fixed and I is a basis of X_i for every i, and the union of I over i is independent, then I is a basis of the union of X_i.

Русский

Если фиксировано множество I и оно является базисом X_i для каждого i, и объединение I по индексу i независимо, тогда I является базисом объединения X_i.

LaTeX

$$$ (\\forall i, M.IsBasis(I, X_i)) \\land M.Indep\\left(\\bigcup_i I\\right) \\Rightarrow M.IsBasis(I, \\bigcup_i X_i) $$$

Lean4

theorem isBasis_iUnion {ι : Type _} [Nonempty ι] (X : ι → Set α) (hI : ∀ i, M.IsBasis I (X i)) :
    M.IsBasis I (⋃ i, X i) :=
  by
  convert IsBasis.iUnion_isBasis_iUnion X (fun _ ↦ I) (fun i ↦ hI i) _ <;> rw [iUnion_const]
  exact (hI (Classical.arbitrary ι)).indep

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