English
If a set of pairs is directed with respect to the first and second coordinates, then the projection onto the second 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_2) (Prod.snd '' d).$$$
Lean4
theorem snd {d : Set (α × β)} (hd : DirectedOn (fun p q ↦ p.1 ≼₁ q.1 ∧ p.2 ≼₂ q.2) d) :
DirectedOn (· ≼₂ ·) (Prod.snd '' d) :=
DirectedOn.mono_comp (fun ⦃_ _⦄ h ↦ h) (mono hd fun ⦃_ _⦄ h ↦ h.2)
