indepSets_of_indepSets_of_le_left

English

If two collections are independent, any subcollection from the left retains independence with the right side.

Русский

Если две коллекции независимы, то любая подколлекция слева сохраняет независимость справа.

LaTeX

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

Lean4

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

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