iicInfHom

Mathlib.Order.UpperLower.Hom

URI: https://scilib.ai/kg/mathlib#LowerSet.iicInfHom

English

The Iic construction yields an InfHom from α to the lower sets: Iic as a mapping to LowerSet α preserves infima.

Русский

Конструкция Iic образует InfHom от α к нижним множествам, сохраняющим инфимы.

LaTeX

$$$ \mathrm{iicInfHom} : \alpha \to \mathrm{InfHom}(\alpha, \mathrm{LowerSet}(\alpha)) $$$

Lean4

/-- `LowerSet.Iic` as an `InfHom`. -/
def iicInfHom : InfHom α (LowerSet α) :=
  ⟨Iic, Iic_inf⟩

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

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

Разделы

Аффилиация

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