of_subsingleton_codomain — Mathlib

English

If ε is a Subsingleton, then for every f: α → ε we have HasFiniteIntegral f μ.

Русский

Если кодомε Subsingleton, тогда для любой f: α → ε выполняется HasFiniteIntegral f μ.

LaTeX

$$([TopologicalSpace ε], [ESeminormedAddMonoid ε], [Subsingleton ε]) ⇒ ∀ f: α → ε, HasFiniteIntegral f μ$$

Lean4

@[simp]
theorem of_subsingleton_codomain {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [Subsingleton ε]
    {f : α → ε} : HasFiniteIntegral f μ :=
  hasFiniteIntegral_zero _ _ |>.congr <| .of_forall fun _ ↦ Subsingleton.elim _ _

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