tau — Mathlib

English

Let τ be the permutation on X' that swaps the coset representing f.hom.range with the infinity point.

Русский

Пусть τ — перестановка на X', которая меняет местами косету, соответствующую f.hom.range, и точку бесконечности.

LaTeX

$$$ \tau : SX' = \text{ Equiv.swap }(\text{fromCoset }⟨\uparrow f.\mathrm{hom}.\mathrm{range}, ⟨1, \text{one_leftCoset }\rangle⟩) \; ∞ $$$

Lean4

/-- Let `τ` be the permutation on `X'` exchanging `f.hom.range` and the point at infinity.
-/
noncomputable def tau : SX' :=
  Equiv.swap (fromCoset ⟨↑f.hom.range, ⟨1, one_leftCoset _⟩⟩) ∞

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