iInter — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iInter {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
    (h : ∃ n, IndepSets (s n) s' κ μ) : IndepSets (⋂ n, s n) s' κ μ := by intro t1 t2 ht1 ht2; obtain ⟨n, h⟩ := h;
  exact h t1 t2 (Set.mem_iInter.mp ht1 n) ht2

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