instSup

Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

URI: https://scilib.ai/kg/mathlib#MeasurableSet.Subtype.instSup

English

There is a supremum operation on the subtype: the supremum of x and y is x ∪ y.

Русский

Существует операция верхней границы над подтипом: наивысшая граница x и y равна x ∪ y.

LaTeX

$$$$x \\lor y = x \\cup y.$$$$

Lean4

instance instSup : Max (Subtype (MeasurableSet : Set α → Prop)) :=
  ⟨fun x y => x ∪ y⟩

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

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

Разделы

Аффилиация

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