instCovariantClassHSMulLe — Mathlib

English

There is a CovariantClass instance for the action of α on Subgroup G with respect to the order on subgroups: the map S ↦ a • S is order-preserving in S.

Русский

Существует класс ковариантности в отношении действия α на Subgroup G, так что отображение S ↦ a • S сохраняет порядок по включению.

LaTeX

$$$\\text{CovariantClass } α (\\mathrm{Subgroup}~G)\\ HSMul.hSMul \\ le$.$$

Lean4

instance : CovariantClass α (Subgroup G) HSMul.hSMul LE.le :=
  ⟨fun _ _ => image_mono⟩

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