inter — Mathlib

English

If s1 and s' are independent, then the intersection with another set s2 is independent.

Русский

Если s1 независимо от s' и s2, то их пересечение независимо от s'.

LaTeX

$$$\\text{CondIndepSets}\\, m' hm' (s_1) s' μ \\Rightarrow \\text{CondIndepSets}\\, m' hm' (s_1 \\cap s_2) s' μ$$$

Lean4

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

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