Questions, not proof records
Each statement record keeps the mathematical question, a dated status source, accessible references, and any pinned Lean formulation separate from proof verification.
sorry marks an admitted statement, not a proof. Source indexing does not mean the formulation has been independently built or certified by Therefore.Does every finite partially ordered set that is not totally ordered contain two elements and such that the probability that appears before in a random linear extension is between and ?
The set of all total order extensions is represented as order preserving bijections of .
The negation of Finite.Equation677_implies_Equation255.
Probably this is true. It would be a stronger form of
Equation677_not_implies_Equation255.
Discussion thread here: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/FINITE.3A.20677.20-.3E.20255
The negation of Finite.Equation677_not_implies_Equation255.
Probably this is false.