Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

FishburnClassicalDefs

Abstract

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

Definition 1.1 (Definition classicalAvoiders).

Lean statement: D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.classicalAvoiders

Formalization. D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.classicalAvoiders (✓ 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 definition specifies a mathematical object used in the Fishburn permutation construction.

Definition 1.2 (Definition claim109).

Lean statement: D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.claim109

Formalization. D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.claim109 (✓ 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 definition specifies a mathematical object used in the Fishburn permutation construction.

Definition 1.3 (Definition claim1011).

Lean statement: D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.claim1011

Formalization. D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.claim1011 (✓ 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 definition specifies a mathematical object used in the Fishburn permutation construction.

Definition 1.4 (Definition claim1012).

Lean statement: D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.claim1012

Formalization. D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.claim1012 (✓ 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 definition specifies a mathematical object used in the Fishburn permutation construction.

References

  • Truth anchor: D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.claim1011
  • Truth anchor: D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.claim1012
  • Truth anchor: D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.claim109
  • Truth anchor: D5/S3/Combinatorics/Fishburn/FishburnClassicalDefs.classicalAvoiders
  • Dependency: D5/S3/Combinatorics/Fishburn/FishburnDefs