measurable_const' — Mathlib

English

If f x = f y for all x,y, then f is measurable.

Русский

Если для всех x,y выполняется f x = f y, то функция измерима.

LaTeX

$$$$ \big( \forall x,y, f x = f y \big) \Rightarrow \mathrm{Measurable}(f) $$$$

Lean4

/-- A version of `measurable_const` that assumes `f x = f y` for all `x, y`. This version works
for functions between empty types. -/
theorem measurable_const' {f : β → α} (hf : ∀ x y, f x = f y) : Measurable f :=
  by
  nontriviality β
  inhabit β
  convert @measurable_const α β _ _ (f default) using 2
  apply hf

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