indepSets_of_indepSets_of_le_left

English

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

Русский

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

LaTeX

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

Lean4

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

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