instIsPretransitiveElemOrbit — Mathlib

English

The action of G on the orbit of a is pretransitive.

Русский

Действие группы G на орбите элемента a является пре-транситивным.

LaTeX

$$IsPretransitive G (orbit G a)$$

Lean4

/-- The action of a group on an orbit is transitive. -/
@[to_additive /-- The action of an additive group on an orbit is transitive. -/
    ]
instance (a : α) : IsPretransitive G (orbit G a) :=
  ⟨by
    rintro ⟨_, g, rfl⟩ ⟨_, h, rfl⟩
    use h * g⁻¹
    ext1
    simp [mul_smul]⟩

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