val_preimage_orbit — Mathlib

English

For m ∈ p, the preimage under the inclusion map of the ambient orbit of m in M equals the orbit of m inside p.

Русский

Для m ∈ p предобраз под включением орбиты m в M равен орбите m внутри p.

LaTeX

$$$ \\mathrm{Subtype.val}^{-1}\\'\\, \\mathrm{MulAction.orbit}\\ R\\ (m : M) = \\mathrm{MulAction.orbit}\\ R\\ m $$$

Lean4

@[to_additive]
theorem val_preimage_orbit {p : SubMulAction R M} (m : p) :
    Subtype.val ⁻¹' MulAction.orbit R (m : M) = MulAction.orbit R m := by
  rw [← val_image_orbit, Subtype.val_injective.preimage_image]

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