dist_map_map_zero_lt — Mathlib

English

For all f,g, dist(f(0) + g(0), f(g(0))) < 1.

Русский

Для любых f,g: расстояние между f(0) + g(0) и f(g(0)) меньше 1.

LaTeX

$$$\forall f,g \in \CircleDeg1Lift:\; \operatorname{dist}(f(0) + g(0), f(g(0))) < 1$$$

Lean4

theorem dist_map_map_zero_lt : dist (f 0 + g 0) (f (g 0)) < 1 :=
  by
  rw [dist_comm, Real.dist_eq, abs_lt, lt_sub_iff_add_lt', sub_lt_iff_lt_add', ← sub_eq_add_neg]
  exact ⟨f.lt_map_map_zero g, f.map_map_zero_lt g⟩

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