indepSets_of_indepSets_of_le_right

English

If s1 independent of s2 and s3 ⊆ s2, then s1 independent of s3.

Русский

Если s1 независим от s2, и s3 ⊆ s2, тогда s1 независим от s3.

LaTeX

$$$\text{IndepSets}(s_1,s_2, μ) \to s_3\subseteq s_2 \Rightarrow \text{IndepSets}(s_1,s_3, μ)$$$

Lean4

theorem indepSets_of_indepSets_of_le_right {s₁ s₂ s₃ : Set (Set Ω)} (h_indep : IndepSets s₁ s₂ μ) (h32 : s₃ ⊆ s₂) :
    IndepSets s₁ s₃ μ :=
  Kernel.indepSets_of_indepSets_of_le_right h_indep h32

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