n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone (graph.proj ∘ ↑(graphEquiv₂ f))
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone (f ∘ ↑(sort f))
rw [self_comp_sort]
no goals
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone (graph.proj ∘ ↑(graphEquiv₂ f))
exact (monotone_proj f).comp (graphEquiv₂ f).monotone