symm — Mathlib

English

Symmetry of CondIndepSets: CondIndepSets m' hm' s1 s2 μ implies CondIndepSets m' hm' s2 s1 μ.

Русский

Симметрия CondIndepSets: независимость между s1 и s2 перенесётся на взаимно противоположную последовательность.

LaTeX

$$$\\text{symm}(h) : CondIndepSets\, m' hm' \\, s_1 \\, s_2 \\, μ \\Rightarrow CondIndepSets\, m' hm' \\, s_2 \\, s_1 \\, μ$$$

Lean4

@[symm]
theorem symm {s₁ s₂ : Set (Set Ω)} (h : CondIndepSets m' hm' s₁ s₂ μ) : CondIndepSets m' hm' s₂ s₁ μ :=
  Kernel.IndepSets.symm h

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