structure definition def or abbrev

`ChannelBundle`

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

formal statement (Lean)

  33structure ChannelBundle (State : Type*) where
  34  Index : Type*
  35  Obs : Index → Type*
  36  channel : (i : Index) → DisplayChannel State (Obs i)
  37
  38namespace ChannelBundle
  39
  40variable {State : Type*}
  41

used by (3)

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

isGloballyOptimal in IndisputableMonolith.RRF.Core.DisplayChannel decl_use
Octave in IndisputableMonolith.RRF.Core.Octave decl_use
trivialChannelBundle in IndisputableMonolith.RRF.Models.Trivial decl_use

depends on (5)

Lean names referenced from this declaration's body.

Index in IndisputableMonolith.Chemistry.PeriodicTable decl_use
State in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
State in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
Index in IndisputableMonolith.Relativity.ILG.Action decl_use
DisplayChannel in IndisputableMonolith.RRF.Core.DisplayChannel decl_use