Autor: José A. Alonso

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

• 1. Si f: ℝ → ℝ es suprayectiva, entonces ∃x ∈ ℝ tal que f(x)² = 9
• 2. La composición de funciones suprayectivas es suprayectiva
• 3. En ℝ, a < b → ¬(b < a)
• 4. Si para cada a existe un x tal que f(x) > a, entonces f no tiene cota superior
• 5. Si para cada a existe un x tal que f(x) < a, entonces f no tiene cota inferior

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (18 de noviembre de 2023)”

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

• 1. Transitividad de la divisibilidad
• 2. Si a divide a b y a c, entonces divide a b+c
• 3. La función (x ↦ x + c) es suprayectiva
• 4. Si c ≠ 0, entonces la función (x ↦ cx) es suprayectiva
• 5. Si c ≠ 0, entonces la función (x ↦ cx + d) es suprayectiva

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (11 de noviembre de 2023)”

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

• 1. La suma de dos funciones acotadas superiormente también lo está
• 2. La suma de dos funciones acotadas inferiormente también lo está
• 3. Si a es una cota superior de f y c ≥ 0, entonces ca es una cota superior de cf
• 4. Si c ≥ 0 y f está acotada superiormente, entonces c·f también lo está
• 5. Si x e y son sumas de dos cuadrados, entonces xy también lo es

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (5 de noviembre de 2023)”

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

• 1. Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s
• 2. La función (x ↦ x + c) es inyectiva
• 3. Si c ≠ 0, entonces la función (x ↦ cx) es inyectiva
• 4. La composición de funciones inyectivas es inyectiva
• 5. Hay algún número real entre 2 y 3

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (28 de octubre de 2023)”