instMeasurableInf

Mathlib.MeasureTheory.Order.Lattice

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

← MathLib Explorer

English

In the dual order, with Max M and MeasurableSup M, infimum is measurable.

Русский

В сопряжённом порядке, с Max M и MeasurableSup M, инфимум измерим.

LaTeX

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

Lean4

instance (priority := 100) instMeasurableInf [Max M] [MeasurableSup M] : MeasurableInf Mᵒᵈ :=
  ⟨@measurable_const_sup M _ _ _, @measurable_sup_const M _ _ _⟩

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

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

Разделы

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

Аффилиация

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