Documentation

Lean 4 Proof

structure CoupledState where
  ρ : ℝ
  T : ℝ
  J_real : ℝ

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:44

Module Section

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

In the same file