prod_sdiff_div_prod_sdiff — Mathlib

English

For any f, s1, s2, (∏ x ∈ s2 \\ s1 f x)/(∏ x ∈ s1 \\ s2 f x) = (∏ x ∈ s2 f x)/(∏ x ∈ s1 f x).

Русский

Для любых f, s1, s2: (∏ x ∈ s2 \\ s1 f x)/(∏ x ∈ s1 \\ s2 f x) = (∏ x ∈ s2 f x)/(∏ x ∈ s1 f x).

LaTeX

$$$$ \\frac{\\prod_{x \\in s_2 \\setminus s_1} f(x)}{\\prod_{x \\in s_1 \\setminus s_2} f(x)} = \\frac{\\prod_{x \\in s_2} f(x)}{\\prod_{x \\in s_1} f(x)} $$$$

Lean4

@[to_additive]
theorem prod_sdiff_div_prod_sdiff : (∏ x ∈ s₂ \ s₁, f x) / ∏ x ∈ s₁ \ s₂, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x := by
  simp [← Finset.prod_sdiff (@inf_le_left _ _ s₁ s₂), ← Finset.prod_sdiff (@inf_le_right _ _ s₁ s₂)]

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