Сформулируем необходимое для следующей теоремы понятие
функции Лобачевского.
Пусть a - прямая на плоскости Лобачевского L2,
A - точка на L2,
не лежащая на прямой a (см. рисунок ниже).
Через точку A проходят две прямые
b1, b2,
параллельные прямой a в различных направлениях.
Прямые b1, b2
образуют равные углы с перпендикуляром AD
к прямой a. Острый угол,
который составляет любая из прямых
b1 или b2
с перпендикуляром AD, называется
углом параллельности при точке A
по отношению к прямой a.
Угол параллельности вполне определяется расстоянием от точки A
до прямой a.
Функция ф = П(x), выражающая меру ф
угла параллельности через длину перпендикуляра AD называется
функцией Лобачевского.
Теорема.
Для функции Лобачевского П(x) имеет место формула