theorem
proved
term proof
preserves_equilibria
show as:
view Lean formalization →
formal statement (Lean)
73theorem preserves_equilibria {O₁ O₂ : Octave}
74 [inst : StrainFunctional.NonNeg O₂.strain]
75 (f : OctaveMorphism O₁ O₂)
76 (x : O₁.State) (hx : O₁.strain.isBalanced x)
77 (hf : O₂.strain.J (f.map x) ≤ O₁.strain.J x) :
78 O₂.strain.isBalanced (f.map x) := by
proof body
Term-mode proof.
79 simp only [StrainFunctional.isBalanced] at *
80 rw [hx] at hf
81 have h₁ := @StrainFunctional.NonNeg.nonneg _ O₂.strain inst (f.map x)
82 linarith
83
84end OctaveMorphism
85
86/-- Two octaves are equivalent if there exist mutually inverse morphisms
87 that both preserve strain exactly (isometric in both directions). -/