theorem
proved
term proof
meissner_effect_structural
show as:
view Lean formalization →
formal statement (Lean)
115theorem meissner_effect_structural
116 (n_s e m c : ℝ) (hns : 0 < n_s) (he : 0 < e) (hm : 0 < m) (hc : 0 < c)
117 (A : ℝ) :
118 -- Supercurrent is proportional to vector potential (London equation)
119 ∃ lL_sq : ℝ, lL_sq = m * c ^ 2 / (4 * Real.pi * n_s * e ^ 2) ∧
120 ∃ j : ℝ, j = -A / lL_sq := by
proof body
Term-mode proof.
121 refine ⟨m * c ^ 2 / (4 * Real.pi * n_s * e ^ 2), rfl, ?_⟩
122 exact ⟨-A / (m * c ^ 2 / (4 * Real.pi * n_s * e ^ 2)), rfl⟩
123
124/-- London penetration depth is positive. -/