map_map_zero_lt — Mathlib

English

For all f,g ∈ CircleDeg1Lift, f(g(0)) is strictly less than f(0) + g(0) + 1: f(g(0)) < f(0) + g(0) + 1.

Русский

Для любых f,g ∈ CircleDeg1Lift верно: f(g(0)) < f(0) + g(0) + 1.

LaTeX

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

Lean4

theorem map_map_zero_lt : f (g 0) < f 0 + g 0 + 1 :=
  calc
    f (g 0) ≤ f 0 + ⌈g 0⌉ := f.map_map_zero_le g
    _ < f 0 + (g 0 + 1) := (add_lt_add_left (ceil_lt_add_one _) _)
    _ = f 0 + g 0 + 1 := (add_assoc _ _ _).symm

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