Сформулируем необходимое для следующей теоремы понятие функции Лобачевского. Пусть a - прямая на плоскости Лобачевского L², A - точка на L², не лежащая на прямой a (см. рисунок ниже).

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

Теорема.
Для функции Лобачевского П(x) имеет место формула