orbit_subgroup_subset — Mathlib

English

For a subgroup H ≤ G and a ∈ α, the H-orbit of a is contained in the G-orbit of a.

Русский

Для подгруппы H ≤ G и элемента a ∈ α орбита H вокруг a содержится в орбите G вокруг a.

LaTeX

$$$$ \\operatorname{orbit}(H, a) \\subseteq \\operatorname{orbit}(G, a). $$$$

Lean4

@[to_additive]
theorem orbit_subgroup_subset (H : Subgroup G) (a : α) : orbit H a ⊆ orbit G a :=
  orbit_submonoid_subset H.toSubmonoid a

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