English
Every element of α lies in some orbit; the universe is the union of all G-orbits.
Русский
Каждый элемент α лежит в некоторой орбите; множество α является объединением всех орбит.
LaTeX
$$$\text{Set.univ} = \bigcup_{x \in Ω} x.\text{orbit}$$$
Lean4
/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action.
Phrased as a set union. See `MulAction.selfEquivSigmaOrbits` for the type isomorphism. -/
@[to_additive /-- Decomposition of a type `X` as a disjoint union of its orbits under an additive
group action. Phrased as a set union. See `AddAction.selfEquivSigmaOrbits` for the type
isomorphism. -/
]
theorem univ_eq_iUnion_orbit : Set.univ (α := α) = ⋃ x : Ω, x.orbit :=
by
ext x
simp only [Set.mem_univ, Set.mem_iUnion, true_iff]
exact ⟨Quotient.mk'' x, by simp⟩
