ωSup_apply_ωSup

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.ContinuousHom.ωSup_apply_ωSup

← MathLib Explorer

English

Same as above, a variant form of the ωSup apply ωSup equality.

Русский

То же самое, альтернативная форма равенства ωSup применений и ωSup.

LaTeX

$$$ (\forall {α}{β},\dots)\;$$

Lean4

theorem ωSup_apply_ωSup (c₀ : Chain (α →𝒄 β)) (c₁ : Chain α) : ωSup c₀ (ωSup c₁) = Prod.apply (ωSup (c₀.zip c₁)) := by
  simp [Prod.apply_apply, Prod.ωSup_zip]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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