of_subsingleton — Mathlib

English

If α is a Subsingleton and μ is a finite measure, then every f: α → β has finite integral: HasFiniteIntegral f μ.

Русский

Если область α состоит из одного элемента (Subsingleton) и мера μ конечна, тогда любой переход: f: α → β имеет конечный интеграл: HasFiniteIntegral f μ.

LaTeX

$$[Subsingleton α] [IsFiniteMeasure μ] ⇒ ∀ f: α → β, HasFiniteIntegral f μ$$

Lean4

theorem of_subsingleton [Subsingleton α] [IsFiniteMeasure μ] {f : α → β} : HasFiniteIntegral f μ :=
  .of_finite

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