instProperSMulSubtypeMemSubgroupOfIsClosedCoe

English

If H is a closed subgroup of G, and G acts properly on X, then H acts properly on X.

Русский

Если H — замкнутая подгруппа G, и G действует корректно на X, то H действует корректно на X.

LaTeX

$$$\\text{ProperSMul } H X$ given$ H\\le G$ замкнутое, и$\\text{ProperSMul } G X$$$

Lean4

/-- If `H` is a closed subgroup of `G` and `G` acts properly on `X`, then so does `H`. -/
@[to_additive /-- If `H` is a closed subgroup of `G` and `G` acts properly on `X`, then so does `H`. -/
    ]
instance {H : Subgroup G} [ProperSMul G X] [H_closed : IsClosed (H : Set G)] : ProperSMul H X :=
  properSMul_of_isClosedEmbedding H.subtype H_closed.isClosedEmbedding_subtypeVal fun _ _ ↦ rfl

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