circleIntegrable_const

Mathlib.MeasureTheory.Integral.CircleIntegral

URI: https://scilib.ai/kg/mathlib#circleIntegrable_const

English

A constant function f ≡ a is CircleIntegrable for any center c and radius R.

Русский

Постоянная функция f ≡ a является CircleIntegrable для любого центра c и радиуса R.

LaTeX

$$$CircleIntegrable\bigl(\lambda z. a, c, R\bigr).$$$

Lean4

@[simp]
theorem circleIntegrable_const (a : E) (c : ℂ) (R : ℝ) : CircleIntegrable (fun _ => a) c R :=
  intervalIntegrable_const

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

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

Разделы

Аффилиация

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