dist_lt_of_dist_lt_modulus

Mathlib.Topology.ContinuousMap.Compact

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

← MathLib Explorer

English

If dist(a,b) is less than the modulus f.modulus ε h, then dist(f(a),f(b)) is less than ε.

Русский

Если dist(a,b) меньше m = f.modulus ε h, то dist(f(a),f(b)) < ε.

LaTeX

$$dist(a,b) < f.modulus(ε,h) ⇒ dist(f(a),f(b)) < ε$$

Lean4

theorem dist_lt_of_dist_lt_modulus (f : C(α, β)) (ε : ℝ) (h : 0 < ε) {a b : α} (w : dist a b < f.modulus ε h) :
    dist (f a) (f b) < ε :=
  (Classical.choose_spec (uniform_continuity f ε h)).2 w

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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