instMeasurableSup₂

Mathlib.MeasureTheory.Order.Lattice

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

English

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

Русский

В двойственном порядке, при Min M и MeasurableInf₂ M, выполняется MeasurableSup₂.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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