instMeasurableSup

Mathlib.MeasureTheory.Order.Lattice

URI: https://scilib.ai/kg/mathlib#OrderDual.instMeasurableSup

← MathLib Explorer

English

In the dual order, with Min M and MeasurableInf M, the supremum is measurable.

Русский

В сопряжённом порядке с Min M и MeasurableInf M сумма-верхняя операция измерима.

LaTeX

$$$\operatorname{MeasurableSup}(M^{\mathrm{op}})$$$

Lean4

instance (priority := 100) instMeasurableSup [Min M] [MeasurableInf M] : MeasurableSup Mᵒᵈ :=
  ⟨@measurable_const_inf M _ _ _, @measurable_inf_const M _ _ _⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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