Documentation

Lean 4 Proof

theorem between_curvature_pos {Ktilde VarRho : ℝ}
    (hK : 0 < Ktilde) (hV : 0 < VarRho) :
    0 < betweenCurvature Ktilde VarRho := by
  exact mul_pos hK hV

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/Closure.lean:75

Module Section

Results 80-85: Rho-Diversity Selection and Closure

In the same file