uniformContinuous_div_const' — Mathlib

English

Let R be a division ring and a ∈ R. The map b ↦ b / a on R is uniformly continuous.

Русский

Пусть R — дивизионное кольцо, и a ∈ R. Отображение b ↦ b/a на R является равномерно непрерывным.

LaTeX

$$$\\forall a \\in R,\\; \\operatorname{UniformContinuous}(b \\mapsto b/a)$$$

Lean4

theorem uniformContinuous_div_const' {R : Type*} [DivisionRing R] [UniformSpace R] [UniformContinuousConstSMul Rᵐᵒᵖ R]
    (a : R) : UniformContinuous fun b : R => b / a :=
  uniformContinuous_id.div_const' _

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