isBasis_setOf_insert_isBasis — Mathlib

English

Let I be a fixed set and suppose I is a basis of X_i for every i, with an independence hypothesis on the union of I. Then I is a basis of the union of X_i.

Русский

Пусть I — фиксированное множество; если для каждого i I является базисом X_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_setOf_insert_isBasis (hI : M.Indep I) : M.IsBasis I {x | M.IsBasis I (insert x I)} :=
  by
  refine
    hI.isBasis_of_forall_insert (fun e he ↦ (?_ : M.IsBasis _ _)) (fun e he ↦ ⟨fun hu ↦ he.2 ?_, he.1.subset_ground⟩)
  · rw [insert_eq_of_mem he]; exact hI.isBasis_self
  simpa using (hu.eq_of_isBasis he.1).symm

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