English
Let α, β be types with β nonempty and Hausdorff. Then a function f: α → β is strongly measurable with respect to the bottom σ-algebra on α if and only if f is constant.
Русский
Пусть α, β — типы, β непуст, β — hausdorff. Тогда функция f: α → β является сильно измеримой относительно нулевой σ-алгебры на α тогда и только тогда, когда она константна.
LaTeX
$$$\mathrm{StronglyMeasurable}_\perp(f) \iff \exists c\in \beta,\ \forall x\in \alpha:\ f(x)=c$$$
Lean4
theorem _root_.stronglyMeasurable_bot_iff [Nonempty β] [T2Space β] : StronglyMeasurable[⊥] f ↔ ∃ c, f = fun _ => c :=
by
rcases isEmpty_or_nonempty α with hα | hα
· simp [eq_iff_true_of_subsingleton]
refine ⟨fun hf => ?_, fun hf_eq => ?_⟩
· refine ⟨f hα.some, ?_⟩
let fs := hf.approx
have h_fs_tendsto : ∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x)) := hf.tendsto_approx
have : ∀ n, ∃ c, ∀ x, fs n x = c := fun n => SimpleFunc.simpleFunc_bot (fs n)
let cs n := (this n).choose
have h_cs_eq : ∀ n, ⇑(fs n) = fun _ => cs n := fun n => funext (this n).choose_spec
conv at h_fs_tendsto => enter [x, 1, n]; rw [h_cs_eq]
have h_tendsto : Tendsto cs atTop (𝓝 (f hα.some)) := h_fs_tendsto hα.some
ext1 x
exact tendsto_nhds_unique (h_fs_tendsto x) h_tendsto
· obtain ⟨c, rfl⟩ := hf_eq
exact stronglyMeasurable_const
