le_ceil_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:\; \lceil f(0) \rceil + \lfloor g(0) \rfloor \le \lceil f(g(0)) \rceil$$$

Lean4

theorem le_ceil_map_map_zero : ⌈f 0⌉ + ⌊g 0⌋ ≤ ⌈(f * g) 0⌉ :=
  calc
    ⌈f 0⌉ + ⌊g 0⌋ = ⌈f 0 + ⌊g 0⌋⌉ := (ceil_add_intCast _ _).symm
    _ ≤ ⌈f (g 0)⌉ := ceil_mono <| f.le_map_map_zero g

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