ceil_map_map_zero_le — Mathlib

English

Let f and g be CircleDeg1Lift. Then the ceiling of f(g(0)) is bounded above by the sum of the ceilings of f(0) and g(0): ⌈f(g(0))⌉ ≤ ⌈f(0)⌉ + ⌈g(0)⌉.

Русский

Пусть f и g — CircleDeg1Lift. Тогда ⌈f(g(0))⌉ ≤ ⌈f(0)⌉ + ⌈g(0)⌉.

LaTeX

$$$\forall f,g \in \CircleDeg1Lift:\; \lceil f(g(0)) \rceil \le \lceil f(0) \rceil + \lceil g(0) \rceil$$$

Lean4

theorem ceil_map_map_zero_le : ⌈f (g 0)⌉ ≤ ⌈f 0⌉ + ⌈g 0⌉ :=
  calc
    ⌈f (g 0)⌉ ≤ ⌈f 0 + ⌈g 0⌉⌉ := ceil_mono <| f.map_map_zero_le g
    _ = ⌈f 0⌉ + ⌈g 0⌉ := ceil_add_intCast _ _

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