def definition def or abbrev

`isGloballyOptimal`

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

formal statement (Lean)

  42def isGloballyOptimal (B : ChannelBundle State) (x : State) : Prop :=

proof body

Definition body.

  43  ∀ i, (B.channel i).isOptimal x
  44
  45end ChannelBundle
  46
  47/-- Two channels are quality-equivalent if they induce the same ordering on states. -/

depends on (4)

Lean names referenced from this declaration's body.

State in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
State in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
ChannelBundle in IndisputableMonolith.RRF.Core.DisplayChannel decl_use
isOptimal in IndisputableMonolith.RRF.Core.DisplayChannel decl_use