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

Equations

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

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

Equations

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

def C03S02.FnHasUb (f : ℝ → ℝ) : Prop

Equations

• C03S02.FnHasUb f = ∃ (a : ℝ), C03S02.FnUb f a

def C03S02.FnHasLb (f : ℝ → ℝ) : Prop

Equations

• C03S02.FnHasLb f = ∃ (a : ℝ), C03S02.FnLb f a

theorem C03S02.fnUb_add {f : ℝ → ℝ} {g : ℝ → ℝ} {a : ℝ} {b : ℝ} (hfa : C03S02.FnUb f a) (hgb : C03S02.FnUb g b) : C03S02.FnUb (fun (x : ℝ) => f x + g x) (a + b)

def C03S02.SumOfSquares {α : Type u_1} [CommRing α] (x : α) : Prop

Equations

• C03S02.SumOfSquares x = ∃ (a : α) (b : α), x = a ^ 2 + b ^ 2

theorem C03S02.sumOfSquares_mul {α : Type u_1} [CommRing α] {x : α} {y : α} (sosx : C03S02.SumOfSquares x) (sosy : C03S02.SumOfSquares y) : C03S02.SumOfSquares (x * y)

theorem C03S02.sumOfSquares_mul' {α : Type u_1} [CommRing α] {x : α} {y : α} (sosx : C03S02.SumOfSquares x) (sosy : C03S02.SumOfSquares y) : C03S02.SumOfSquares (x * y)