instBoundedOrder

Mathlib.Analysis.BoxIntegral.Partition.Filter

URI: https://scilib.ai/kg/mathlib#BoxIntegral.IntegrationParams.instBoundedOrder

English

GP is below every IntegrationParams element; i.e., GP is the bottom element of the order.

Русский

GP является нижним элементом порядка; GP ≤ l для любого l.

LaTeX

$$$\\text{GP} \\le l$ for all l.$$

Lean4

instance : BoundedOrder IntegrationParams :=
  isoProd.symm.toGaloisInsertion.liftBoundedOrder

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

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

Разделы

Аффилиация

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