sup

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#CompleteLattice.ωScottContinuous.sup

Lean4

theorem sup (hf : ωScottContinuous f) (hg : ωScottContinuous g) : ωScottContinuous (f ⊔ g) :=
  by
  rw [← sSup_pair]
  apply ωScottContinuous.sSup
  rintro f (rfl | rfl | _) <;> assumption

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

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

Разделы

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

Аффилиация

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