Выписываем, что значит для круга двигаться по плоскости касаясь прямой, определяем движение без проскальзывания и выводим оттуда
. Если считать прямую неподвижной, это будет ограничение свойств непрерывного семейства изометрических отображений
какой-то плоскости с нарисованным на ней кругом на плоскость, на которой нарисована прямая. Можно замечательно формализовать всё, но вообще формула довольно интуитивная без привлечения всего такого.
Я думал в этом направлении, но такой подход не даёт ответа, как не сводить определение к одному из эквивалентных свойств (которые мы как раз хотим вывести).
Качение без проскальзывания - это когда мгновенная ось вращения колеса всегда есть точка контакта колеса и поверхности.
Видимо, это подходит. Спасибо.