instIsBoundedSMulSeparationQuotient

English

If α acts boundedly on β, then it acts boundedly on the separation quotient of β.

Русский

Если на β действует ограниченно α, то на сепарации β действует ограниченно α.

LaTeX

$$$IsBoundedSMul(\\alpha, \\text{SeparationQuotient}(\\beta))$$$

Lean4

instance {α β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [IsBoundedSMul α β] :
    IsBoundedSMul α (SeparationQuotient β)
    where
  dist_smul_pair' _ := Quotient.ind₂ <| dist_smul_pair _
  dist_pair_smul' _
    _ :=
    Quotient.ind <|
      dist_pair_smul _
        _
          -- We don't have the `SMul α γ → SMul β δ → SMul (α × β) (γ × δ)` instance, but if we did, then
          -- `IsBoundedSMul α γ → IsBoundedSMul β δ → IsBoundedSMul (α × β) (γ × δ)` would hold

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