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

costCompose_no_identity

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)

 161theorem costCompose_no_identity :
 162    ¬ ∃ e : ℝ, 0 ≤ e ∧ ∀ a : ℝ, 0 ≤ a → e ★ a = a := by

proof body

Tactic-mode proof.

 163  intro h
 164  rcases h with ⟨e, he_nonneg, he⟩
 165  have h0 : e ★ 0 = 0 := he 0 le_rfl
 166  rw [costCompose_zero_right] at h0
 167  have he0 : e = 0 := by
 168    linarith
 169  have h1 : (0 : ℝ) ★ 1 = 1 := by
 170    simpa [he0] using he 1 (by positivity)
 171  rw [costCompose_zero_left] at h1
 172  norm_num at h1
 173
 174/-- Third-power associativity: the triple `★`-power is unambiguous. -/

depends on (7)

Lean names referenced from this declaration's body.