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)
58theorem refl (C : DisplayChannel State Obs₁) : QualityEquiv C C :=
proof body
Term-mode proof.
59 fun _ _ => Iff.rfl
60
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
-
DisplayChannel
in IndisputableMonolith.RRF.Core.DisplayChannel
decl_use
-
QualityEquiv
in IndisputableMonolith.RRF.Core.DisplayChannel
decl_use