## Stream: new members

### Topic: how to function composition

#### Michael Nestor (Jan 10 2023 at 01:25):

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 (Jan 10 2023 at 01:26):

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

#### Sky Wilshaw (Jan 10 2023 at 01:26):

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

#### Michael Nestor (Jan 10 2023 at 01:27):

I am trying to apply is_limit to the sequence f a

#### Sky Wilshaw (Jan 10 2023 at 01:27):

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

#### Sky Wilshaw (Jan 10 2023 at 01:27):

I think you need to parenthesise f ∘ a.

#### Sky Wilshaw (Jan 10 2023 at 01:28):

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

#### Michael Nestor (Jan 10 2023 at 01:29):

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 (Jan 10 2023 at 01:30):

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

Last updated: Dec 20 2023 at 11:08 UTC