volume_ball — Mathlib

English

Identify C with R^2; the area of a disk in the complex plane of radius r is π r^2.

Русский

Идентифицируя комплексное число с точкой R^2, площадь дискa радиуса r в комплексной плоскости равна π r^2.

LaTeX

$$$$ \operatorname{vol}(\mathrm{ball}(a,r)) = \pi r^{2} $$$$

Lean4

@[simp]
theorem volume_ball (a : ℂ) (r : ℝ) : volume (Metric.ball a r) = .ofReal r ^ 2 * NNReal.pi := by
  simp [InnerProductSpace.volume_ball_of_dim_even (k := 1) (by simp) a, ← NNReal.coe_real_pi, ofReal_coe_nnreal]

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