instOrderBot

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.instOrderBot

English

There is an OrderBot structure on Germ(l, β) induced from β.

Русский

На Germ(l, β) существует порядок-бот, индуцированный β.

LaTeX

$$$\\mathrm{OrderBot}(\\mathrm{Germ}(l,\\beta))$$$

Lean4

instance instOrderBot [LE β] [OrderBot β] : OrderBot (Germ l β) where
  bot_le f := inductionOn f fun _ => Eventually.of_forall fun _ => bot_le

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

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

Разделы

Аффилиация

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