theorem C03S01.my_lemma (x : ℝ) (y : ℝ) (ε : ℝ) : 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε

theorem C03S01.my_lemma2 {x : ℝ} {y : ℝ} {ε : ℝ} : 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε

theorem C03S01.my_lemma3 {x : ℝ} {y : ℝ} {ε : ℝ} : 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε

theorem C03S01.my_lemma4 {x : ℝ} {y : ℝ} {ε : ℝ} : 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε

def C03S01.FnUb (f : ℝ → ℝ) (a : ℝ) : Prop

Equations

• C03S01.FnUb f a = ∀ (x : ℝ), f x ≤ a

def C03S01.FnLb (f : ℝ → ℝ) (a : ℝ) : Prop

Equations

• C03S01.FnLb f a = ∀ (x : ℝ), a ≤ f x

def C03S01.FnUb' {α : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid R] (f : α → R) (a : R) : Prop

Equations

• C03S01.FnUb' f a = ∀ (x : α), f x ≤ a

theorem C03S01.fnUb_add {α : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid R] {f : α → R} {g : α → R} {a : R} {b : R} (hfa : C03S01.FnUb' f a) (hgb : C03S01.FnUb' g b) : C03S01.FnUb' (fun (x : α) => f x + g x) (a + b)

def C03S01.FnEven (f : ℝ → ℝ) : Prop

Equations

• C03S01.FnEven f = ∀ (x : ℝ), f x = f (-x)

def C03S01.FnOdd (f : ℝ → ℝ) : Prop

Equations

• C03S01.FnOdd f = ∀ (x : ℝ), f x = -f (-x)

theorem C03S01.Subset.refl {α : Type u_1} (s : Set α) : s ⊆ s

theorem C03S01.Subset.trans {α : Type u_1} (r : Set α) (s : Set α) (t : Set α) : r ⊆ s → s ⊆ t → r ⊆ t

def C03S01.SetUb {α : Type u_1} [PartialOrder α] (s : Set α) (a : α) : Prop

Equations

• C03S01.SetUb s a = ∀ x ∈ s, x ≤ a