indepSets_of_indepSets_of_le_right

English

If s1 independent from s2, then any s3 ⊆ s2 is independent from s1 as well.

Русский

Если s1 независимо от s2, то любая подмножество s3 ⊆ s2 независимо от s1.

LaTeX

$$$ h\\_indep : IndepSets s1 s2 κ μ \\Rightarrow h32 : s3 \\subseteq s2 \\Rightarrow IndepSets s1 s3 κ μ $$$

Lean4

theorem indepSets_of_indepSets_of_le_right {s₁ s₂ s₃ : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω}
    {μ : Measure α} (h_indep : IndepSets s₁ s₂ κ μ) (h32 : s₃ ⊆ s₂) : IndepSets s₁ s₃ κ μ := fun t1 t2 ht1 ht2 =>
  h_indep t1 t2 ht1 (Set.mem_of_subset_of_mem h32 ht2)

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