uniformContinuous_map₂ — Mathlib

English

In the abstract completion context, the map₂ constructed from uniformly continuous maps is uniformly continuous.

Русский

В контексте абстрактного дополнения отображение map₂, построенное из равномерно непрерывных отображений, равномерно непрерывно.

LaTeX

$$$ \forall f, \text{UniformContinuous}_2 (pkg.map_2\ pkg'\ pkg'' f)$$$

Lean4

theorem uniformContinuous_map₂ (f : α → β → γ) : UniformContinuous₂ (pkg.map₂ pkg' pkg'' f) :=
  AbstractCompletion.uniformContinuous_extension₂ pkg pkg' _

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