pith. machine review for the scientific record. sign in
theorem proved term proof

superfluid_fraction_at_lambda

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 127theorem superfluid_fraction_at_lambda (Tlam : ℝ) (hTlam : 0 < Tlam) :
 128    superfluid_fraction Tlam Tlam = 0 := by

proof body

Term-mode proof.

 129  unfold superfluid_fraction
 130  simp [div_self (ne_of_gt hTlam), Real.one_rpow]
 131
 132/-- For 0 < T < Tlam, fraction is strictly between 0 and 1. -/

depends on (8)

Lean names referenced from this declaration's body.