English
If two sets are directed under their respective orders, then their product set is directed under coordinate-wise order.
Русский
Если множества направлены в своих порядках, то их произведение направлено по координатному порядку.
LaTeX
$$$\forall d_1:d_1\, \forall d_2: d_2, DirectedOn(\lambda p q, (p.1,q.1) \le (q.1,p.2)) (d_1 \times d_2).$$$
Lean4
theorem prod {d₁ : Set α} {d₂ : Set β} (h₁ : DirectedOn (· ≼₁ ·) d₁) (h₂ : DirectedOn (· ≼₂ ·) d₂) :
DirectedOn (fun p q ↦ p.1 ≼₁ q.1 ∧ p.2 ≼₂ q.2) (d₁ ×ˢ d₂) := fun _ hpd _ hqd =>
by
obtain ⟨r₁, hdr₁, hpr₁, hqr₁⟩ := h₁ _ hpd.1 _ hqd.1
obtain ⟨r₂, hdr₂, hpr₂, hqr₂⟩ := h₂ _ hpd.2 _ hqd.2
exact ⟨⟨r₁, r₂⟩, ⟨hdr₁, hdr₂⟩, ⟨hpr₁, hpr₂⟩, ⟨hqr₁, hqr₂⟩⟩
