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)
47def wellPosed : Prop := ∃ x : O.State, O.strain.isBalanced x
proof body
Definition body.
48
49end Octave
50
51/-- A morphism between octaves: a map that preserves strain ordering. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (12)
Lean names referenced from this declaration's body.
-
State
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
isBalanced
in IndisputableMonolith.Cosmology.DarkEnergy
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
map
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
State
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
that
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
isBalanced
in IndisputableMonolith.RRF.Core.Glossary
decl_use
-
Octave
in IndisputableMonolith.RRF.Core.Octave
decl_use
-
isBalanced
in IndisputableMonolith.RRF.Core.Strain
decl_use
-
isBalanced
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use