English
If a family of directed sets with a product structure is directed, then projecting to a coordinate preserves directedness.
Русский
Если множество в произведении направлено относительно компонент, то проекция на одну координату сохраняет направленность.
LaTeX
$$$\forall d: Set(\Pi i, \alpha_i), \ DirectedOn(\lambda x, x_i)''d) \Rightarrow DirectedOn (r_i) (Set.image(\lambda a, a_i) d).$$$
Lean4
theorem proj {d : Set (Π i, α i)} (hd : DirectedOn (fun x y => ∀ i, r i (x i) (y i)) d) (i : ι) :
DirectedOn (r i) ((fun a => a i) '' d) :=
DirectedOn.mono_comp (fun _ _ h => h) (mono hd fun ⦃_ _⦄ h ↦ h i)
