English
If a set of pairs is directed with respect to the first and second coordinates, then the projection onto the first coordinate is directed.
Русский
Если множество пар направлено по координатам, проекция на первую координату направлена.
LaTeX
$$$\forall d: Set(\Alpha \times \Beta), DirectedOn( (p,q) \mapsto p.1 \preceq_1 q.1 \land p.2 \preceq_2 q.2 ) d \Rightarrow DirectedOn (\le_1) (Prod.fst '' d).$$$
Lean4
theorem fst {d : Set (α × β)} (hd : DirectedOn (fun p q ↦ p.1 ≼₁ q.1 ∧ p.2 ≼₂ q.2) d) :
DirectedOn (· ≼₁ ·) (Prod.fst '' d) :=
DirectedOn.mono_comp (fun ⦃_ _⦄ h ↦ h) (mono hd fun ⦃_ _⦄ h ↦ h.1)
