pi — Mathlib · SciLib

English

Let π be the real number defined as twice a zero of the cosine function in the interval [1,2]. It is the usual constant π.

Русский

Пусть π — вещественное число, определяемое как удвоенное значение нуля косинуса на интервале [1,2]. Это обычное число π.

LaTeX

$$$\exists x \in [1,2], \cos x = 0 \wedge \pi = 2x$$$

Lean4

/-- The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened. -/
protected noncomputable def pi : ℝ :=
  2 * Classical.choose exists_cos_eq_zero

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