how to function composition

Stream: new members

[Michael Nestor]

some basic calculus:

import data.nat.basic
import data.real.basic
def is_limit (a: ℕ → ℝ) (L: ℝ) :=
  ∀ ε: ℝ, ∃ n : ℕ, ∀ m : ℕ, m >= n → |a n - L| < ε
def is_continuous (f: ℝ → ℝ) :=
∀ x: ℝ, ∀ a: ℕ → ℝ, ∀ L: ℝ, is_limit a L → is_limit f ∘ a f L

fails on f ∘ a: type mismatch at application is_limit f, term f has type ℝ → ℝ but is expected to have type ℕ → ℝ

[Sky Wilshaw]

is_limit is the definition of a limit of a sequence, not the limit of a function as you approach a point.

[Sky Wilshaw]

ℕ → ℝ is the type of real sequences, and ℝ → ℝ is the type of real-valued functions on the real line.

[Michael Nestor]

I am trying to apply is_limit to the sequence f a

[Sky Wilshaw]

Ah, you're using the sequence definition of continuity, I see.

[Sky Wilshaw]

I think you need to parenthesise f ∘ a.

[Sky Wilshaw]

I think the correct RHS is is_limit a L → is_limit (f ∘ a) (f L).

[Michael Nestor]

ok yep def is_continuous (f: ℝ → ℝ) := ∀ x: ℝ, ∀ a: ℕ → ℝ, ∀ L: ℝ, is_limit a L → is_limit (f ∘ a) (f L) worked. finally understand how multiple arguments work! lol

[Sky Wilshaw]

Function application "binds tighter" than basically anything else. a b <op> c d is always parsed (a b) <op> (c d).