stronglyMeasurable_const' — Mathlib

English

In a setting with One, the constant one function is strongly measurable.

Русский

В условиях с единицей, константная функция 1 является сильно измеримой.

LaTeX

$$$\\text{StronglyMeasurable}(1_{\\alpha \\to \\beta})$$$

Lean4

/-- A version of `stronglyMeasurable_const` that assumes `f x = f y` for all `x, y`.
This version works for functions between empty types. -/
theorem stronglyMeasurable_const' (hf : ∀ x y, f x = f y) : StronglyMeasurable f :=
  by
  nontriviality α
  inhabit α
  convert stronglyMeasurable_const (β := β) using 1
  exact funext fun x => hf x default

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