octubre 2023 – Página 3

En ℝ, {0 < ε, ε ≤ 1, |x| < ε, |y| < ε} ⊢ |xy| < ε

PorJosé A. Alonso 3 octubre 202313 septiembre 2023

Demostrar con Lean4, que en ℝ
\[ \left\{ 0 < ε, ε ≤ 1, |x| < ε, |y| < ε \right\} ⊢ |xy| < ε \] Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic

example :
  ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
by sorry

import Mathlib.Data.Real.Basic

example :

∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=

by sorry

PorJosé A. Alonso 2 octubre 202311 septiembre 2023

Demostrar con Lean4 que en los espacios métricos, \(d(x,y) ≥ 0\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Topology.MetricSpace.Basic
variable {X : Type _} [MetricSpace X]
variable (x y : X)

example : 0 ≤ d x y :=
by sorry

import Mathlib.Topology.MetricSpace.Basic

variable {X : Type _} [MetricSpace X]

variable (x y : X)

example : 0 ≤ d x y :=

by sorry