prod

Mathlib.Order.SupClosed

URI: https://scilib.ai/kg/mathlib#InfClosed.prod

English

If s and t are inf-closed, then their product s × t is inf-closed.

Русский

Если s и t инф-замкнуты, то их произведение инф-замкнуто.

LaTeX

$$$ (\\text{InfClosed } s) \\rightarrow (\\text{InfClosed } t) \\rightarrow \\text{InfClosed}(s \\times t) $$$

Lean4

theorem prod {t : Set β} (hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ×ˢ t) := fun _a ha _b hb ↦
  ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩

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

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

Разделы

Аффилиация

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