selfEquivSigmaOrbits — Mathlib

English

There is a canonical equivalence between α and a sigma-type of its orbits, refining the previous decomposition.

Русский

Существуют канонические эквивалентности между α и сигма-типом орбит, уточняющие предыдущее разложение.

LaTeX

$$def selfEquivSigmaOrbits : α ≃ Σ ω : Ω, orbit G ω.out$$

Lean4

/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action. -/
@[to_additive /-- Decomposition of a type `X` as a disjoint union of its orbits under an additive
    group action. -/
    ]
def selfEquivSigmaOrbits : α ≃ Σ ω : Ω, orbit G ω.out :=
  (selfEquivSigmaOrbits' G α).trans <|
    Equiv.sigmaCongrRight fun _ => Equiv.setCongr <| orbitRel.Quotient.orbit_eq_orbit_out _ Quotient.out_eq'

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