condIndepSets_of_condIndepSets_of_le_left

English

If CondIndepSets holds for s1 with respect to s2, and s3 ⊆ s1, then CondIndepSets also holds for s3 with respect to s2.

Русский

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

LaTeX

$$$h\\_indep : CondIndepSets\, m' hm'\, s_1\, s_2\, μ \\;\n\\; h_{31} : s_3 \\subseteq s_1 \\Rightarrow CondIndepSets\, m' hm'\, s_3\, s_2\, μ$$$

Lean4

theorem condIndepSets_of_condIndepSets_of_le_left {s₁ s₂ s₃ : Set (Set Ω)} (h_indep : CondIndepSets m' hm' s₁ s₂ μ)
    (h31 : s₃ ⊆ s₁) : CondIndepSets m' hm' s₃ s₂ μ :=
  Kernel.indepSets_of_indepSets_of_le_left h_indep h31

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