instOrderTop

Mathlib.Analysis.BoxIntegral.Partition.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Prepartition.instOrderTop

Lean4

instance : OrderTop (Prepartition I) where
  top := single I I le_rfl
  le_top π _ hJ := ⟨I, by simp, π.le_of_mem hJ⟩

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

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

Разделы

Аффилиация

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