Theorem: TrussDesign.F₁ₚ_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 < F₁ₚ
Tactic:
unfold F₁ₚ
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 < 10

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 < 10
Tactic:
norm_num
State after:
no goals