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)
83def consistentStates {State : Type*} (SL : StrainLedger State) : Set State :=
proof body
Definition body.
84 { x | isConsistent SL x }
85
86end RRF.Core
87end IndisputableMonolith
depends on (6)
Lean names referenced from this declaration's body.
-
State
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
RRF
in IndisputableMonolith.Foundation.Hamiltonian
decl_use
-
State
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
isConsistent
in IndisputableMonolith.RRF.Core.Glossary
decl_use
-
StrainLedger
in IndisputableMonolith.RRF.Core.Strain
decl_use
-
isConsistent
in IndisputableMonolith.RRF.Foundation.Consciousness
decl_use