Examples and distinctions
Constructed examples of this model; each answer includes the Lean statement.
Exact root statement
∀ {Potential : Type u} {State : Type v} {Density : Type w} (data : GroundStateComparison Potential State Density)
(left right : State) (number : ℕ),
data.NondegenerateGroundStateAtParticleNumber left number →
data.NondegenerateGroundStateAtParticleNumber right number →
data.densityOf left = data.densityOf right →
data.NonconstantPotentialsGiveDistinctGroundStates →
data.GroundStateEnergyEquation →
data.PotentialEnergyDifferenceEquation →
data.StrictNondegenerateVariationalPrinciple →
data.ConstantShiftPreservesGroundStates → data.NondegenerateGroundStateUniqueness → left = right
Compare two arguments
Compare their definitions and hypotheses. Shared declarations may be instantiated differently; differences do not establish equivalence or implication.
No comparison argument selected.
Compare an earlier extraction
Compare the displayed specifications with an earlier JSON export. This compares text, not mathematical equivalence. Files stay in this browser.
No earlier extraction selected.
Notes and questions
Import merges local entries without overwriting them.
All declarations in the selected argument
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structure
- structure
- structure
- structure
- structure
- structure
Definitions and domain choices
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Constructors, projections, and other meaning dependencies
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary