val_image_orbit — Mathlib

English

The orbit of m in p, when mapped into M via the underlying inclusion, coincides with the ambient orbit of m in M.

Русский

Орбита m внутри p, отображённая в M через вложение, совпадает с орбитой m в M.

LaTeX

$$$ \\mathrm{Set.image}(\\mathrm{Subtype.val}, \\mathrm{MulAction.orbit}\\ R\\ m) = \\mathrm{MulAction.orbit}\\ R\\ (m : M) $$$

Lean4

/-- Orbits in a `SubMulAction` coincide with orbits in the ambient space. -/
@[to_additive]
theorem val_image_orbit {p : SubMulAction R M} (m : p) :
    Subtype.val '' MulAction.orbit R m = MulAction.orbit R (m : M) :=
  (Set.range_comp _ _).symm

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