continuous_probChar

Mathlib.Analysis.Complex.Circle

URI: https://scilib.ai/kg/mathlib#Real.continuous_probChar

English

The map x ↦ probChar(x) is continuous.

Русский

Отображение x ↦ probChar(x) непрерывно.

LaTeX

$$$\mathrm{probChar}: \mathbb{R} \to \mathbb{C}$ is continuous.$$

Lean4

@[continuity]
theorem continuous_probChar : Continuous probChar :=
  Circle.exp.continuous

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru