Proving continuity of elementary functions

Stream: new members

[Duncan Skahan]

How do I prove continuity of an elementary function? continuity isn't working for me.

import Mathlib

noncomputable section

def f (x : ℝ) := x + 1

theorem test: Continuous f := by
  continuity

#check test

I'm getting the error tactic 'aesop' failed, failed to prove the goal after exhaustive search.

[Notification Bot]

A message was moved here from #new members > ✔ How to prove basic continuity statements? by Duncan Skahan.

[Kevin Buzzard]

I suspect Lean will not unfold that f unless explicitly asked (which would explain the error because you defined f but didn't prove any theorems about it). Probably unfold f or simp [f] will enable continuity but there might be tricks like continuity [f] (not sure, this is not a tactic I use much and I'm not at lean right now)

[Kevin Buzzard]

Or changing def f to abbrev f (which aesop will unfold) would also probably work

[Duncan Skahan]

Thank you. unfold f worked.

[Jireh Loreaux]

Also, you'll likely prefer to use fun_prop instead of continuity.