condIndepSets_of_condIndepSets_of_le_right

English

If CondIndepSets m' hm' s1 s2 μ holds and s3 ⊆ s2, then CondIndepSets m' hm' s1 s3 μ holds.

Русский

Если CondIndepSets выполняется для s1 и s2, и s3 ⊆ s2, то CondIndepSets выполняется для s1 и s3.

LaTeX

$$$h_indep : CondIndepSets\, m' hm'\, s_1\, s_2\, μ \\;\\Rightarrow\\; h_{32} : s_3 \\subseteq s_2 \\Rightarrow CondIndepSets\, m' hm'\, s_1\, s_3\, μ$$$

Lean4

theorem condIndepSets_of_condIndepSets_of_le_right {s₁ s₂ s₃ : Set (Set Ω)} (h_indep : CondIndepSets m' hm' s₁ s₂ μ)
    (h32 : s₃ ⊆ s₂) : CondIndepSets m' hm' s₁ s₃ μ :=
  Kernel.indepSets_of_indepSets_of_le_right h_indep h32

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