English
If two antitone 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 antitone, then } f \\circ σ = f \\circ τ.$$$
Lean4
/-- If two permutations of a tuple `f` are both antitone, then they are equal. -/
theorem unique_antitone [PartialOrder α] {f : Fin n → α} {σ τ : Equiv.Perm (Fin n)} (hfσ : Antitone (f ∘ σ))
(hfτ : Antitone (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
