English
If two monotone compositions f ∘ σ and f ∘ τ coincide, then they are equal: f ∘ σ = f ∘ τ.
Русский
Если две монотонные композиции[f ∘ σ] и [f ∘ τ] совпадают, то они равны: f ∘ σ = f ∘ τ.
LaTeX
$$$\\text{If } (f \\circ σ) \\text{ and } (f \\circ τ) \\text{ are monotone, then } f \\circ σ = f \\circ τ.$$$
Lean4
/-- If two permutations of a tuple `f` are both monotone, then they are equal. -/
theorem unique_monotone [PartialOrder α] {f : Fin n → α} {σ τ : Equiv.Perm (Fin n)} (hfσ : Monotone (f ∘ σ))
(hfτ : Monotone (f ∘ τ)) : f ∘ σ = f ∘ τ :=
ofFn_injective <|
eq_of_perm_of_sorted ((σ.ofFn_comp_perm f).trans (τ.ofFn_comp_perm f).symm) hfσ.ofFn_sorted hfτ.ofFn_sorted
