Theorem: TrussDesign.σₚ_pos (CvxLean/Examples/TrussDesign.lean)

State before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < σₚ
Tactic:
unfold σₚ
State after:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 0.5

State before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 0.5
Tactic:
norm_num
State after:
no goals