measurableSup — Mathlib

English

If γ is a topological space with a max operation and a continuous supremum, then the supremum operator is measurable.

Русский

Пусть γ — топологическое пространство с операцией максимума и непрерывной верхней гранью; тогда операция перехода к верхнему пределу измерима.

LaTeX

$$$\text{MeasurableSup}(\gamma)$$$

Lean4

instance (priority := 100) measurableSup [Max γ] [ContinuousSup γ] : MeasurableSup γ
    where
  measurable_const_sup _ := (continuous_const.sup continuous_id).measurable
  measurable_sup_const _ := (continuous_id.sup continuous_const).measurable

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