English
If each component is directed, then the pi-type of directed relations is directed.
Русский
Если каждое целочисленное множество направлено, то произведение по индексу тоже направлено.
LaTeX
$$$\forall d : (i:\iota) \to Set(\alpha_i), (\forall i, DirectedOn (r_i) (d_i)) \Rightarrow DirectedOn (\forall i, r_i) (Set.univ.\pi d).$$$
Lean4
theorem pi {d : (i : ι) → Set (α i)} (hd : ∀ (i : ι), DirectedOn (r i) (d i)) :
DirectedOn (fun x y => ∀ i, r i (x i) (y i)) (Set.pi Set.univ d) :=
by
intro a ha b hb
choose f hfd haf hbf using fun i => hd i (a i) (ha i trivial) (b i) (hb i trivial)
exact ⟨f, fun i _ => hfd i, haf, hbf⟩
