probChar_ne_one

Mathlib.Analysis.Complex.Circle

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

English

probChar is not identically equal to the constant 1; in particular, probChar(π) ≠ 1.

Русский

probChar не является тождественно равной единице; например, probChar(π) ≠ 1.

LaTeX

$$$\exists x \in \mathbb{R}: \operatorname{probChar}(x) \neq 1$$$

Lean4

theorem probChar_ne_one : probChar ≠ 1 := by
  rw [DFunLike.ne_iff]
  use Real.pi
  simpa only [probChar_apply'] using Circle.exp_pi_ne_one

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

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

Разделы

Аффилиация

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