union — Mathlib

English

If a collection s1 is independent from s' and a collection s2 is independent from s' (both with respect to μ), then their union (as a collection) is independent from s' (μ).

Русский

Если коллекции \$s_1\$ и \$s_2\$ независимы от \$s'\$ относительно меры μ, то их объединение как коллекции независимо от \$s'\$.

LaTeX

$$$IndepSets(s_1, s'; \\mu) \\land IndepSets(s_2, s'; \\mu) \\Rightarrow IndepSets(s_1 \\cup s_2, s'; \\mu)$$$

Lean4

theorem union {s₁ s₂ s' : Set (Set Ω)} (h₁ : IndepSets s₁ s' μ) (h₂ : IndepSets s₂ s' μ) : IndepSets (s₁ ∪ s₂) s' μ :=
  Kernel.IndepSets.union h₁ h₂

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