of_discrete — Mathlib

English

There exists a surjective map from Nat onto a countable type α used to build a strongly measurable representation

Русский

Существует сюръективное отображение натурала на счетное множество α, используемое в построении сильно измеримой оценки.

LaTeX

$$∃ g: ℕ → α, surjective(g) ⇒ StronglyMeasurable f$$

Lean4

@[fun_prop]
theorem of_discrete [Countable α] : StronglyMeasurable f :=
  by
  nontriviality α
  nontriviality β
  obtain ⟨g, hg⟩ := exists_surjective_nat α
  exact ⟨simpleFuncAux f g, hg.forall.2 fun m ↦ tendsto_nhds_of_eventually_eq simpleFuncAux_eventuallyEq⟩

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