one_sub_K_pos'

Mathlib.Topology.MetricSpace.Contracting

URI: https://scilib.ai/kg/mathlib#ContractingWith.one_sub_K_pos'

English

If a map f is contracting with constant K, then 1 − K is a positive extended nonnegative real.

Русский

Если отображение сжимает с константой K, то 1 − K является положительным неотрицательным числом.

LaTeX

$$$ (0 : \mathbb{R}_{\ge 0}^{\infty}) < 1 - K $$$

Lean4

theorem one_sub_K_pos' (hf : ContractingWith K f) : (0 : ℝ≥0∞) < 1 - K := by simp [hf.1]

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

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

Разделы

Аффилиация

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