disjointSum_isBasis_iff — Mathlib

English

A pair (I,X) is a basis for the disjointSum iff fiberwise bases hold in each M_i and the global inclusions I ⊆ X ⊆ ⋃ E_i.

Русский

Пара (I,X) является базисом для disjointSum тогда и только тогда, когда по волокнам в каждом M_i выполняются базисы и выполняются глобальные включения I ⊆ X ⊆ ⋃ E_i.

LaTeX

$$$$ (M.disjointSum N h).IsBasis I X \iff (\forall i, (M i).IsBasis (I \cap (M i).E) (X \cap (M i).E)) \land I \subseteq X \land X \subseteq ⋃ i\,(M i).E. $$$$

Lean4

@[simp]
theorem disjointSum_isBasis_iff {h I X} :
    (M.disjointSum N h).IsBasis I X ↔
      M.IsBasis (I ∩ M.E) (X ∩ M.E) ∧ N.IsBasis (I ∩ N.E) (X ∩ N.E) ∧ I ⊆ X ∧ X ⊆ M.E ∪ N.E :=
  by simp [disjointSum, and_assoc]

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