simpleFunc_bot' — Mathlib

English

Any simple function with bottom MeasurableSpace is equal to a constant simple function.

Русский

Любая простая функция с нижним пространством измеримости равна константной простой функции.

LaTeX

$$$\\exists c, f = \\mathrm{SimpleFunc.const}(\\alpha, \\, \\bot, \\, c)$$$

Lean4

theorem simpleFunc_bot' {α} [Nonempty β] (f : @SimpleFunc α ⊥ β) : ∃ c, f = @SimpleFunc.const α _ ⊥ c :=
  letI : MeasurableSpace α := ⊥;
  (simpleFunc_bot f).imp fun _ ↦ ext

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