lemma proved term proof

`pressure_eq_proxy`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  59lemma pressure_eq_proxy (P : PressureParams) [H : PressureDropFromVorticity P] (S : MediumState) :
  60    H.pressure S = pressureProxy P S :=

proof body

Term-mode proof.

  61  H.pressure_eq S
  62
  63end Pressure
  64end Flight
  65end IndisputableMonolith
  66

depends on (8)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
MediumState in IndisputableMonolith.Flight.Medium decl_use
PressureDropFromVorticity in IndisputableMonolith.Flight.Pressure decl_use
PressureParams in IndisputableMonolith.Flight.Pressure decl_use
pressureProxy in IndisputableMonolith.Flight.Pressure decl_use
pressure in IndisputableMonolith.ILG.PressureForm decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use