Documentation

Lean 4 Proof

theorem cycleProductReal_pos {N : ℕ} {k : Fin N → ℝ} (hk : ∀ n, 0 < k n) :
    0 < cycleProductReal N k :=
  Finset.prod_pos fun n _ => hk n

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:134

Module Section

## Entry-Exit Core Definitions (merged from EntryExitDefs.lean)

In the same file