FishburnTenNineClassicalSplit

Abstract

Mathematical definitions and results for Fishburn permutations and classical pattern avoidance.

Theorem 1.1 (Theorem avoids231_maxSplit_iff).

Lean statement: D5/S3/Combinatorics/Fishburn/FishburnTenNineClassicalSplit.avoids231_maxSplit_iff

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Fishburn/FishburnTenNineClassicalSplit.avoids231_maxSplit_iff (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Eric S. Egge (2022). Pattern-Avoiding Fishburn Permutations and Ascent Sequences. DOI: 10.48550/arXiv.2208.01484. URL: https://arxiv.org/abs/2208.01484v1.

Commentary.

This theorem establishes the stated mathematical relation for Fishburn permutations and classical pattern avoidance.

Theorem 1.2 (Theorem avoids4123_maxSplit_iff).

Lean statement: D5/S3/Combinatorics/Fishburn/FishburnTenNineClassicalSplit.avoids4123_maxSplit_iff

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Fishburn/FishburnTenNineClassicalSplit.avoids4123_maxSplit_iff (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Eric S. Egge (2022). Pattern-Avoiding Fishburn Permutations and Ascent Sequences. DOI: 10.48550/arXiv.2208.01484. URL: https://arxiv.org/abs/2208.01484v1.

Commentary.

This theorem establishes the stated mathematical relation for Fishburn permutations and classical pattern avoidance.

Truth anchor: D5/S3/Combinatorics/Fishburn/FishburnTenNineClassicalSplit.avoids231_maxSplit_iff
Truth anchor: D5/S3/Combinatorics/Fishburn/FishburnTenNineClassicalSplit.avoids4123_maxSplit_iff
Dependency: D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs