inter — Mathlib

English

If s1 is independent from s′, then s1 ∩ s2 is independent from s′.

Русский

Если s1 независимо от s′, то s1 ∩ s2 независимо от s′.

LaTeX

$$IndepSets(s1, s', κ, μ) ⇒ IndepSets(s1 ∩ s2, s', κ, μ)$$

Lean4

theorem inter {s₁ s' : Set (Set Ω)} (s₂ : Set (Set Ω)) {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
    (h₁ : IndepSets s₁ s' κ μ) : IndepSets (s₁ ∩ s₂) s' κ μ := fun t1 t2 ht1 ht2 =>
  h₁ t1 t2 ((Set.mem_inter_iff _ _ _).mp ht1).left ht2

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