def
definition
def or abbrev
ResonantAxes
show as:
view Lean formalization →
formal statement (Lean)
30def ResonantAxes : Set (Fin 3 → ℝ) :=
proof body
Definition body.
31 { fun i => if i = 0 then 1 else 0
32 , fun i => if i = 1 then 1 else 0
33 , fun i => if i = 2 then 1 else 0 }
34
35/-- **DEFINITION: Alignment Quality**
36 Measure of how well the postural axis matches a resonant axis. -/