Documentation

Lean 4 Proof

def CoupledState.feasible (s : CoupledState) : Prop :=
  s.ρ < 1 ∧ 0 ≤ s.T ∧ 1 < s.J_real

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:50

Module Section

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

In the same file