En ℝ, {0 < ε, ε ≤ 1, |x| < ε, |y| < ε} ⊢ |xy| < ε
Demostrar con Lean4, que en ℝ
\[ \left\{ 0 < ε, ε ≤ 1, |x| < ε, |y| < ε \right\} ⊢ |xy| < ε \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by sorry |
Read More «En ℝ, {0 < ε, ε ≤ 1, |x| < ε, |y| < ε} ⊢ |xy| < ε"