union_iff — Mathlib

English

IndepSets holds for the union s1 ∪ s2 if and only if it holds for s1 and for s2 separately.

Русский

IndepSets выполняется для объединения s1 ∪ s2 тогда и только тогда, когда он выполняется отдельно для s1 и для s2.

LaTeX

$$IndepSets(s1 ∪ s2, s', κ, μ) ↔ (IndepSets(s1, s', κ, μ) ∧ IndepSets(s2, s', κ, μ))$$

Lean4

@[simp]
theorem union_iff {s₁ s₂ s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} :
    IndepSets (s₁ ∪ s₂) s' κ μ ↔ IndepSets s₁ s' κ μ ∧ IndepSets s₂ s' κ μ :=
  ⟨fun h =>
    ⟨indepSets_of_indepSets_of_le_left h Set.subset_union_left,
      indepSets_of_indepSets_of_le_left h Set.subset_union_right⟩,
    fun h => IndepSets.union h.left h.right⟩

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