toIcoDiv_zero_one — Mathlib

English

For a zero-to-b one-parameter family, the IcoDiv reduces to the floor of b, i.e., it matches the integer part of b when p = 1.

Русский

Для случая p = 1 разбиение по интервалу сводится к целой части числа b: IcoDiv = ⌊b⌋.

LaTeX

$$$$ \\operatorname{toIcoDiv}(\\text{zero\_lt\_one}'(\\alpha), 0, b) = \\Big\\lfloor b \\Big\\rfloor $$$$

Lean4

theorem toIcoDiv_zero_one (b : α) : toIcoDiv (zero_lt_one' α) 0 b = ⌊b⌋ := by simp [toIcoDiv_eq_floor]

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