reorderRestrictProd_of_compl — Mathlib

English

A simple lemma about restricting by complement and identifying components.

Русский

Простая лемма об ограничении по дополнению и идентификации компонент.

LaTeX

$$$\operatorname{restrict\_compl}(S,s,p) = p.1$$$

Lean4

@[simp]
theorem reorderRestrictProd_of_compl (p : Sᶜ.restrict '' s × (Π i : S, α i)) (j : (Sᶜ : Set ι)) :
    reorderRestrictProd S s p j = (p.1 : Π j : ↑(Sᶜ : Set ι), α j) j :=
  by
  have hj : ↑j ∉ S := j.prop
  simp [reorderRestrictProd, hj]

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