symmetryEquiv — Mathlib

English

There is a symmetry equivalence between the j-fibers of the two π maps, i.e., between preimages under π c2 c1 c12 and π c1 c2 c12 for the same j.

Русский

Существует эквивалентность симметрии между соответствующими волоками фиксированного j для карт π, то есть между их предобразами.

LaTeX

$$$\\text{symmetryEquiv}(j):\\ (π_{c_2,c_1,c_{12}}^{-1}\\{j\\}) \\simeq (π_{c_1,c_2,c_{12}}^{-1}\\{j\\}).$$$

Lean4

/-- The symmetry bijection `(π c₂ c₁ c₁₂ ⁻¹' {j}) ≃ (π c₁ c₂ c₁₂ ⁻¹' {j})`. -/
@[simps]
def symmetryEquiv (j : I₁₂) : (π c₂ c₁ c₁₂ ⁻¹' { j }) ≃ (π c₁ c₂ c₁₂ ⁻¹' { j })
    where
  toFun := fun ⟨⟨i₂, i₁⟩, h⟩ => ⟨⟨i₁, i₂⟩, by simpa [π_symm] using h⟩
  invFun := fun ⟨⟨i₁, i₂⟩, h⟩ => ⟨⟨i₂, i₁⟩, by simpa [π_symm] using h⟩

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