uniformContinuous

Mathlib.Topology.UniformSpace.UniformEmbedding

URI: https://scilib.ai/kg/mathlib#IsUniformInducing.uniformContinuous

English

From IsUniformInducing, one derives UniformContinuous f.

Русский

Из IsUniformInducing следует UniformContinuous f.

LaTeX

$$$\\text{UniformContinuous } f$$$

Lean4

theorem uniformContinuous {f : α → β} (hf : IsUniformInducing f) : UniformContinuous f :=
  (isUniformInducing_iff'.1 hf).1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru