modulus_pos

Mathlib.Topology.ContinuousMap.Compact

URI: https://scilib.ai/kg/mathlib#ContinuousMap.modulus_pos

English

For a fixed ε>0, the modulus f.modulus ε h is positive.

Русский

Для любого ε>0 модуль f.modulus ε является положительным.

LaTeX

$$0 < f.modulus(ε,h)$$

Lean4

theorem modulus_pos (f : C(α, β)) {ε : ℝ} {h : 0 < ε} : 0 < f.modulus ε h :=
  (Classical.choose_spec (uniform_continuity f ε h)).1

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

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

Разделы

Аффилиация

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