of_subsingleton_cod — Mathlib

English

If the codomain β has at most one element, then every function f: α → β is ae-strongly measurable with respect to μ (i.e., AEStronglyMeasurable f μ).

Русский

Если кодом β обладает не более чем одним элементом (subsingleton), то любая функция f: α → β является ae‑строго измеримой по отношению к μ.

LaTeX

$$$[\\text{Subsingleton}(\\beta)] \\Rightarrow \\operatorname{AEStronglyMeasurable}_m(f, \\mu)$$$

Lean4

@[simp, nontriviality]
theorem of_subsingleton_cod [Subsingleton β] : AEStronglyMeasurable[m] f μ :=
  StronglyMeasurable.of_subsingleton_cod.aestronglyMeasurable

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