Prove the Brahmagupta-Fibonacci identity \[ (a^2 + b^2)(c^2 + d^2) = (ac - bd)^2 + (ad + bc)^2 \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c d : ℝ) example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 := sorry
Let \(x, y ∈ ℝ\). Prove that \[ (∀ ε > 0, y ≤ x + ε) → y ≤ x \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {x y : ℝ} example : (∀ ε > 0, y ≤ x + ε) → y ≤ x := by sorry
In Lean4, one can define that \(x\) is an upper bound of \(A\) by
def is_upper_bound (A : Set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x
and \(x\) is supremum of \(A\) by
def is_supremum (A : Set ℝ) (x : ℝ) := is_upper_bound A x ∧ ∀ y, is_upper_bound A y → x ≤ y
Prove that if \(x\) is the supremum of \(A\), then \[ (∀ y)[y < x → (∃ a ∈ A)[y < a]] \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic variable {A : Set ℝ} variable {x : ℝ} def is_upper_bound (A : Set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x def is_supremum (A : Set ℝ) (x : ℝ) := is_upper_bound A x ∧ ∀ y, is_upper_bound A y → x ≤ y example (hx : is_supremum A x) : ∀ y, y < x → ∃ a ∈ A, y < a := by sorry