theorem
proved
term proof
conserved_iff_conserved'
show as:
view Lean formalization →
formal statement (Lean)
82theorem conserved_iff_conserved' {X : Type*} (Q : X → ℝ) (φ : ℝ → X → X)
83 (h0 : ∀ x, φ 0 x = x) :
84 IsConservedAlong Q φ ↔ IsConservedAlong' Q φ := by
proof body
Term-mode proof.
85 constructor
86 · intro h t
87 funext x
88 simp only [Function.comp_apply]
89 rw [h x t 0, h0 x]
90 · intro h x t₁ t₂
91 have ht1 := congr_fun (h t₁) x
92 have ht2 := congr_fun (h t₂) x
93 simp only [Function.comp_apply] at ht1 ht2
94 rw [ht1, ht2]
95
96/-! ## Noether's Core Result -/
97
98/-- A 1-parameter group action (simplified model). -/