theorem proved wrapper

`frc_holds_on_RS_lattice`

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

formal statement (Lean)

  95theorem frc_holds_on_RS_lattice (s : FiniteVolumeProfile) : RSLatticeFRC s :=

One-line wrapper that applies finiteVolume_Jcost_bound.

  96  finiteVolume_Jcost_bound s
  97

From the project-wide theorem graph. These declarations reference this one in their body.

frcBridgeCert in IndisputableMonolith.NavierStokes.FRCBridge decl_use
frc_holds_on_RS_lattice_exists in IndisputableMonolith.NavierStokes.FRCBridge decl_use
lattice_regular_via_direction_constancy in IndisputableMonolith.NavierStokes.FRCBridge decl_use

Lean names referenced from this declaration's body.

finiteVolume_Jcost_bound in IndisputableMonolith.NavierStokes.FRCBridge decl_use
FiniteVolumeProfile in IndisputableMonolith.NavierStokes.FRCBridge decl_use
RSLatticeFRC in IndisputableMonolith.NavierStokes.FRCBridge decl_use