mem_subgroup_orbit_iff — Mathlib

English

The SMUL action map from G to the orbit map on x.orbit is compatible with restriction.

Русский

Отображение умножения на орбиту совместимо с ограничением.

LaTeX

$$mapsTo_smul_orbit(g, x) : Set.MapsTo (g • ·) x.orbit x.orbit$$

Lean4

@[to_additive (attr := norm_cast, simp)]
theorem mem_subgroup_orbit_iff {H : Subgroup G} {x : orbitRel.Quotient G α} {a b : x.orbit} :
    (a : α) ∈ MulAction.orbit H (b : α) ↔ a ∈ MulAction.orbit H b :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rcases h with ⟨g, h⟩
    dsimp at h
    rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h
    subst h
    exact MulAction.mem_orbit _ g
  · rcases h with ⟨g, rfl⟩
    exact MulAction.mem_orbit _ g

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