supClosed_range

Mathlib.Order.SupClosed

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

English

The range of a sup-preserving map is sup-closed.

Русский

Образ гомоморфизма, сохраняющего ⊔, замкнут по ⊔.

LaTeX

$$$ \\text{SupClosed} (\\operatorname{range} f) $ (for any sup-homomorphism f).$$

Lean4

theorem supClosed_range [FunLike F α β] [SupHomClass F α β] (f : F) : SupClosed (Set.range f) := by
  simpa using supClosed_univ.image f

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

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

Разделы

Аффилиация

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