orbitRel_apply — Mathlib

English

Let G act on α. The orbit relation between a and b holds exactly when a lies in the G-orbit of b.

Русский

Пусть G действует на α. Отношение орбит между a и b выполняется тогда, когда a принадлежит орбите b под действием G.

LaTeX

$$$a \sim_G b \;\Longleftrightarrow\; a \in G \cdot b$$$

Lean4

@[to_additive]
theorem orbitRel_apply {a b : α} : orbitRel G α a b ↔ a ∈ orbit G b :=
  Iff.rfl

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