infClosed_range

Mathlib.Order.SupClosed

URI: https://scilib.ai/kg/mathlib#infClosed_range

English

The range of an inf-preserving map is inf-closed.

Русский

Образ инф-гомоморфизма инф-замкнут.

LaTeX

$$$ \\text{InfClosed (\\operatorname{range} f)} $$$

Lean4

theorem infClosed_range [FunLike F α β] [InfHomClass F α β] (f : F) : InfClosed (Set.range f) := by
  simpa using infClosed_univ.image f

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

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

Разделы

Аффилиация

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