measurable — Mathlib

English

If a function f: β → α between suitable ordered topological spaces is antitone (order-reversing and monotone with respect to the opposite order), then f is a measurable map between the corresponding Borel spaces.

Русский

Если функция f: β → α между подходящими упорядоченными топологическими пространствами антитоническая (обратный порядок), то она измерима между соответствующими борелевскими пространствами.

LaTeX

$$$\\text{Antitone}(f) \\Rightarrow \\text{Measurable}(f)$$$

Lean4

protected theorem measurable [LinearOrder β] [OrderClosedTopology β] {f : β → α} (hf : Antitone f) : Measurable f :=
  @Monotone.measurable αᵒᵈ β _ _ ‹_› _ _ _ _ _ ‹_› _ _ _ hf

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