inter — Mathlib

English

If s1 is independent from s' and s2 is independent from s', then s1 ∩ s2 is independent from s'.

Русский

Если \$s_1\$ независим от \$s'\$, а \$s_2\$ независим от \$s'\$, то \$s_1 \\cap s_2\$ независим от \$s'\$.

LaTeX

$$$IndepSets(s_1, s'; \\mu) \\rightarrow IndepSets(s_1 \\cap s_2, s'; \\mu)$$$

Lean4

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

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