mul_floor_map_zero_le_floor_iterate_zero

English

For all f and n ∈ ℕ, ↑n · ⌊f(0)⌋ ≤ ⌊f^[n](0)⌋.

Русский

Для всех f и n ∈ ℕ, n · ⌊f(0)⌋ ≤ ⌊f^[n](0)⌋.

LaTeX

$$$\forall f:\CircleDeg1Lift, \forall n \in \mathbb{N}: \; (n) \cdot \lfloor f(0) \rfloor \le \lfloor f^{[n]}(0) \rfloor$$$

Lean4

theorem mul_floor_map_zero_le_floor_iterate_zero (n : ℕ) : ↑n * ⌊f 0⌋ ≤ ⌊f^[n] 0⌋ :=
  by
  rw [le_floor, Int.cast_mul, Int.cast_natCast, ← zero_add ((n : ℝ) * _)]
  apply le_iterate_of_add_int_le_map
  simp [floor_le]

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