measurableSup₂

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

URI: https://scilib.ai/kg/mathlib#ContinuousSup.measurableSup₂

English

In a product-like setting, the two-variable measurable supremum is measurable.

Русский

В обстановке, близкой к произведению, измеримая двойная верхняя грань измерима.

LaTeX

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

Lean4

instance (priority := 100) measurableSup₂ [SecondCountableTopology γ] [Max γ] [ContinuousSup γ] : MeasurableSup₂ γ :=
  ⟨continuous_sup.measurable⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru