An Extreme Value in the Inverse Image

Abstract

A maximal first entry of the inverse image determines the last entry of the original permutation.

Theorem 1.1 (A terminal one).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverseTail.B_first_max_forces_last_one

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverseTail.B_first_max_forces_last_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kassie Archer, Robert P. Laudone (2024). Pattern avoidance and the fundamental bijection. DOI: 10.48550/arXiv.2407.06338. URL: https://arxiv.org/abs/2407.06338v1.

Commentary.

For a nonempty permutation p, if its inverse image under the fundamental bijection starts with the maximum, then p ends with one.

References

• Truth anchor: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverseTail.B_first_max_forces_last_one
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverse