Documentation

Lean 4 Proof

theorem institutionalQuality_pos {tree_coeff : ℝ} {J : ℕ} {Fbar : ℝ}
    (hc : 0 < tree_coeff) (hJ : 2 ≤ J) (hF : 0 < Fbar) :
    0 < institutionalQuality tree_coeff J Fbar := by
  simp only [institutionalQuality]
  apply mul_pos
  · apply mul_pos hc
    exact Nat.cast_pos.mpr (by omega)
  · exact hF

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/Defs.lean:206

Module Section

Core definitions for the Lean formalization of Paper 4:

In the same file