Menu Close

En los espacios métricos, d(x,y) ≥ 0

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

En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc

Demostrar con Lean4 que, en los anillos ordenados,
\[ \{a ≤ b, 0 ≤ c\} ⊢ ac ≤ bc \]

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

import Mathlib.Algebra.Order.Ring.Defs
variable {R : Type _} [StrictOrderedRing R]
variable (a b c : R)
 
example
  (h1 : a  b)
  (h2 : 0  c)
  : a * c  b * c :=
by sorry

En los anillos ordenados, 0 ≤ b – a → a ≤ b

Demostrar con Lean4 que en los anillos ordenados
\[ 0 ≤ b – a → a ≤ b \]

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

import Mathlib.Algebra.Order.Ring.Defs
variable {R : Type _} [StrictOrderedRing R]
variable (a b c : R)
 
example : 0  b - a  a  b :=
by sorry

En los anillos ordenados, a ≤ b → 0 ≤ b – a

Demostrar con Lean4 que en los anillos ordenados se verifica que
\[ a ≤ b → 0 ≤ b – a \]

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

import Mathlib.Algebra.Order.Ring.Defs
variable {R : Type _} [StrictOrderedRing R]
variable (a b c : R)
 
example : a  b  0  b - a :=
by sorry

En los retículos, una distributiva del supremo implica la otra

Demostrar con Lean4 que si \(R\) es un retículo tal que
\[ (∀ x,\ y,\ z \in R) [x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)] \]
entonces
\[ (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) \]
para todos los elementos del retículo.

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

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (a b c : α)
 
example
  (h :  x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y)(x ⊔ z))
  : (a ⊓ b) ⊔ c = (a ⊔ c)(b ⊔ c) :=
by sorry