orbit_eq_iff — Mathlib

English

For G acting on α, orbit G a = orbit G b iff a ∈ orbit G b.

Русский

Для действия G на α: орбита a равна орбите b тогда и только тогда, когда a ∈ orbit G b.

LaTeX

$$$$ \\operatorname{orbit}(G, a) = \\operatorname{orbit}(G, b) \\iff a \\in \\operatorname{orbit}(G, b). $$$$

Lean4

@[to_additive]
theorem orbit_eq_iff {a b : α} : orbit G a = orbit G b ↔ a ∈ orbit G b :=
  ⟨fun h => h ▸ mem_orbit_self _, fun ⟨_, hc⟩ => hc ▸ orbit_smul _ _⟩

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