simpleFunc_bot — Mathlib

English

A simple func from α to ⊥ with β nonempty is constant.

Русский

Простая функция из α в ⊥ с непустым β есть константа.

LaTeX

$$$\\exists c, \\forall x, f(x)=c$$$

Lean4

theorem simpleFunc_bot {α} (f : @SimpleFunc α ⊥ β) [Nonempty β] : ∃ c, ∀ x, f x = c :=
  by
  have hf_meas := @SimpleFunc.measurableSet_fiber α _ ⊥ f
  simp_rw [MeasurableSpace.measurableSet_bot_iff] at hf_meas
  exact (exists_eq_const_of_preimage_singleton hf_meas).imp fun c hc ↦ congr_fun hc

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