theorem proved term proof

`superfluid_fraction_at_zero`

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

formal statement (Lean)

 121theorem superfluid_fraction_at_zero (Tlam : ℝ) (hTlam : 0 < Tlam) :
 122    superfluid_fraction 0 Tlam = 1 := by

Term-mode proof.

 123  unfold superfluid_fraction
 124  simp [Real.zero_rpow (ne_of_gt rs_critical_exponent_positive)]
 125
 126/-- At T = Tlam, normal fluid. -/

Lean names referenced from this declaration's body.

T in IndisputableMonolith.Foundation.Breath1024 decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
rs_critical_exponent_positive in IndisputableMonolith.Physics.Superfluidity decl_use
superfluid_fraction in IndisputableMonolith.Physics.Superfluidity decl_use