orbitRel — Mathlib

English

The relation r a b defined by a ∈ orbit G b is an equivalence relation, i.e., the same-orbit relation.

Русский

Отношение r, определяемое как a ∈ orbit G b, является эквиверенцией: принадлежит одной орбите.

LaTeX

$$$$ \\text{orbitRel }(G, \\alpha) = \\{ (a,b) \\mid a \\in \\operatorname{orbit}(G, b) \\}. $$$$

Lean4

/-- The relation 'in the same orbit'. -/
@[to_additive /-- The relation 'in the same orbit'. -/
    ]
def orbitRel : Setoid α where
  r a b := a ∈ orbit G b
  iseqv :=
    ⟨mem_orbit_self, fun {a b} => by simp [orbit_eq_iff.symm, eq_comm], fun {a b} => by
      simp +contextual [orbit_eq_iff.symm]⟩

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