le_floor_map_map_zero — Mathlib

English

For all f,g, ⌊f(0)⌋ + ⌊g(0)⌋ ≤ ⌊f(g(0))⌋.

Русский

Для всех f,g выполняется ⌊f(0)⌋ + ⌊g(0)⌋ ≤ ⌊f(g(0))⌋.

LaTeX

$$$\forall f,g \in \CircleDeg1Lift:\; \lfloor f(0) \rfloor + \lfloor g(0) \rfloor \le \lfloor f(g(0)) \rfloor$$$

Lean4

theorem le_floor_map_map_zero : ⌊f 0⌋ + ⌊g 0⌋ ≤ ⌊f (g 0)⌋ :=
  calc
    ⌊f 0⌋ + ⌊g 0⌋ = ⌊f 0 + ⌊g 0⌋⌋ := (floor_add_intCast _ _).symm
    _ ≤ ⌊f (g 0)⌋ := floor_mono <| f.le_map_map_zero g

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