Meses: noviembre 2023

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

• 1. La función identidad no está acotada superiormente
• 2. Si f es monótona y f(a) < f(b), entonces a < b
• 3. Si a, b ∈ ℝ tales que a ≤ b y f(b) < f(a), entonces f no es monótona
• 4. No para toda f : ℝ → ℝ monótona, (∀a,b)(f(a) ≤ f(b) → a ≤ b)
• 5. Si (∀ε > 0)(x ≤ ε), entonces x ≤ 0

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

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)”