Saltar al Contenido

Calculemus

Ejercicios de demostración asistida por ordenador

Twitter YouTube Github
Calculemus
Ejercicios de demostración asistida por ordenador

Si 0 < 0, entonces a > 37 para cualquier número a

PorJosé A. Alonso 8 diciembre 202328 noviembre 2023

Demostrar con Lean4 que si \(0 < 0\), entonces \(a > 37\) para cualquier número \(a\).

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

Lean
1
2
3
4
5
6
7
8
import Mathlib.Tactic
 
variable (a : ℕ)
 
example
  (h : 0 < 0)
  : a > 37 :=
by sorry

Read More «Si 0 < 0, entonces a > 37 para cualquier número a»

diciembre 2023
L M X J V S D
 123
45678910
11121314151617
18192021222324
25262728293031
« Nov   Ene »

Últimas entradas

  • Si (∀n)[uₙ ≤ vₙ], entonces lim uₙ ≤ lim vₙ
  • Si x, y ∈ ℝ tales que (∀ z)[y < z → x ≤ z], entonces x ≤ y
  • La paradoja del barbero
  • Las sucesiones convergentes están acotadas
  • Un número es par si y solo si lo es su cuadrado
  • Los supremos de las sucesiones crecientes son sus límites
  • Si `f(x) ≤ f(y) → x ≤ y`, entonces f es inyectiva
  • Si una función es creciente e involutiva, entonces es la identidad
  • La composición de una función creciente y una decreciente es decreciente
  • Los monoides booleanos son conmutativos
  • Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)^n
  • Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c
  • Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a
  • Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹
  • Unicidad de los inversos en los grupos
  • Unicidad del elemento neutro en los grupos
  • Caracterización de producto igual al primer factor
  • Unicidad de inversos en monoides
  • Equivalencia de inversos iguales al neutro
  • Producto de potencias de la misma base en monoides

Correo electrónico

Introduce tu correo electrónico para suscribirte a este blog y recibir notificaciones de nuevas entradas.

RSS feed

© 2020-2025 Calculemus

Scroll to top
Búsqueda