bInter — Mathlib

English

If there exists n ∈ u with IndepSets(s_n, s′, κ, μ), then IndepSets(⋂ n ∈ u, s_n) s' κ μ.

Русский

Если существует n ∈ u с IndepSets(s_n, s′, κ, μ), то пересечение по n ∈ u сохраняет независимость.

LaTeX

$$∃ n ∈ u, IndepSets(s_n, s', κ, μ) ⇒ IndepSets(⋂ n ∈ u, s_n, s', κ, μ)$$

Lean4

theorem bInter {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
    {u : Set ι} (h : ∃ n ∈ u, IndepSets (s n) s' κ μ) : IndepSets (⋂ n ∈ u, s n) s' κ μ :=
  by
  intro t1 t2 ht1 ht2
  rcases h with ⟨n, hn, h⟩
  exact h t1 t2 (Set.biInter_subset_of_mem hn ht1) ht2

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