disjointSum_indep_iff — Mathlib

English

Independence for disjointSum is described fiberwise: I is independent iff its fiber in each component is independent and I sits inside the union of component grounds.

Русский

Независимость для disjointSum описывается по волокнам: I независимо тогда и только тогда, когда его волокно в каждом компоненте независимо и I лежит внутри объединения оснований компонент.

LaTeX

$$$$ (M.disjointSum N h).Indep I \iff M.Indep (I \cap M.E) \land N.Indep (I \cap N.E) \land I \subseteq M.E \cup N.E. $$$$

Lean4

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

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