pith. machine review for the scientific record. sign in
lemma proved tactic proof

G_even_of_reciprocal_symmetry

show as:
view Lean formalization →

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)

  42lemma G_even_of_reciprocal_symmetry
  43  (F : ℝ → ℝ)
  44  (hSymm : ∀ {x : ℝ}, 0 < x → F x = F x⁻¹) :
  45  Function.Even (G F) := by

proof body

Tactic-mode proof.

  46  intro t
  47  have hpos : 0 < Real.exp t := Real.exp_pos t
  48  have hrec : Real.exp (-t) = (Real.exp t)⁻¹ := by simp [Real.exp_neg]
  49  simp [G, hrec, hSymm hpos]
  50

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.