English
The join on β is Scott-continuous in both arguments.
Русский
Складывая join в β по двум аргументам, получаем Scott–непрерывность.
LaTeX
$$$\\mathrm{ScottContinuousOn}(D, (a,b)\\mapsto a \\sqcup b).$$$
Lean4
/-- The join operation is Scott continuous -/
theorem sup₂ : ScottContinuous fun b : β × β => (b.1 ⊔ b.2 : β) := fun d _ _ ⟨p₁, p₂⟩ hdp =>
by
simp only [IsLUB, IsLeast, upperBounds, Prod.forall, mem_setOf_eq, Prod.mk_le_mk] at hdp
simp only [IsLUB, IsLeast, upperBounds, mem_image, Prod.exists, forall_exists_index, and_imp]
have e1 : (p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x} := hdp.2
simp only [lowerBounds, mem_setOf_eq, Prod.forall, Prod.mk_le_mk] at e1
refine ⟨fun a b₁ b₂ hbd hba => ?_, fun b hb => ?_⟩
· rw [← hba]
exact sup_le_sup (hdp.1 _ _ hbd).1 (hdp.1 _ _ hbd).2
· rw [sup_le_iff]
exact e1 _ _ fun b₁ b₂ hb' => sup_le_iff.mp (hb b₁ b₂ hb' rfl)
