reorderRestrictProd_restrict_compl

English

If you start from a restricted element coming from a restriction of a restricted product, applying the inverse of the reorder map returns the original element.

Русский

Для x ∈ S^c.restrict ⁻¹' (S^c.restrict '' s) выполняется, что reorderRestrictProd S s ⟨⟨S^c.restrict x, x.2⟩, ...⟩ = x.

LaTeX

$$$\\text{If } x \\in S^{c}.\\restrict \\, ⋅, \\text{ then }\\ reorderRestrictProd\\,S\\,s\\,{\\langle{\\langle S^{c}.\\restrict x, x.2\\rangle, \\dots} \\rangle} = x.$$$

Lean4

@[simp]
theorem reorderRestrictProd_restrict_compl (x : Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s)) :
    reorderRestrictProd S s ⟨⟨Sᶜ.restrict x, x.2⟩, fun i ↦ (x : Π j, α j) i⟩ = (x : Π j, α j) := by ext;
  simp [reorderRestrictProd]

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