Si para cada a existe un x tal que f(x) > a, entonces f no tiene cota superior

José A. Alonso

16-11-2023

Funciones reales

Demostrar con Lean4 que si \(f\) es una función de \(ℝ\) en \(ℝ\) tal que para cada \(a\) existe un \(x\) tal que \(f(x) > a\), entonces \(f\) no tiene cota superior.

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def acotadaSup (f : ℝ → ℝ) : Prop :=
  ∃ a, CotaSuperior f a

variable (f : ℝ → ℝ)

example
  (h : ∀ a, ∃ x, f x > a)
  : ¬ acotadaSup f :=
by sorry

En ℝ, a < b → ¬(b < a)

José A. Alonso

15-11-2023

Números reales

Demostrar con Lean4 que en \(ℝ\), \(a < b → ¬(b < a)\).

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

import Mathlib.Data.Real.Basic

variable (a b : ℝ)

example
  (h : a < b)
  : ¬ b < a :=
by sorry

La composición de funciones suprayectivas es suprayectiva

José A. Alonso

14-11-2023

Funciones

Demostrar con Lean4 que la composición de funciones suprayectivas es suprayectiva.

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

import Mathlib.Tactic
open Function
variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

example
  (hg : Surjective g)
  (hf : Surjective f)
  : Surjective (g ∘ f) :=
by sorry

Si f es una función real suprayectiva, entonces existe x ∈ ℝ tal que f(x)² = 9

José A. Alonso

13-11-2023

Funciones reales

Demostrar con Lean4 que si \(f: ℝ → ℝ\) es suprayectiva, entonces \(∃x ∈ ℝ\) tal que \(f(x)² = 9\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

open Function

example
  {f : ℝ → ℝ}
  (h : Surjective f)
  : ∃ x, (f x)^2 = 9 :=
by sorry

Si c ≠ 0, entonces la función (x ↦ cx + d) es suprayectiva

José A. Alonso

10-11-2023

Funciones reales

Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx + d\) es suprayectiva.

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

import Mathlib.Data.Real.Basic

variable {c d : ℝ}

open Function

example
  (h : c ≠ 0)
  : Surjective (fun x ↦ c * x + d) :=
by sorry

Si c ≠ 0, entonces la función (x ↦ cx) es suprayectiva

José A. Alonso

09-11-2023

Funciones reales

Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx\) es suprayectiva.

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

import Mathlib.Data.Real.Basic
variable {c : ℝ}
open Function

example
  (h : c ≠ 0)
  : Surjective (fun x ↦ c * x) :=
by sorry

La función (x ↦ x + c) es suprayectiva

José A. Alonso

08-11-2023

Funciones reales

Demostrar con Lean4 que la función \(x ↦ x + c\) es suprayectiva.

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {c : ℝ}

open Function

example : Surjective (fun x ↦ x + c) :=
by sorry

Si a divide a b y a c, entonces divide a b+c

José A. Alonso

07-11-2023

Números naturales

Demostrar con Lean4 que si \(a\) divide a \(b\) y a \(c\), entonces divide a \(b+c\).

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

import Mathlib.Tactic

variable {a b c : ℕ}

example
  (h1 : a ∣ b)
  (h2 : a ∣ c)
  : a ∣ (b + c) :=
by sorry

Transitividad de la divisibilidad

José A. Alonso

06-11-2023

Números naturales

Demostrar con Lean4 la transitividad de la divisibilidad.

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

import Mathlib.Tactic

variable {a b c : ℕ}

example
  (divab : a ∣ b)
  (divbc : b ∣ c) :
  a ∣ c :=
by sorry

Si x e y son sumas de dos cuadrados, entonces xy también lo es

José A. Alonso

03-11-2023

Números naturales

Demostrar con Lean4 que si \(x\) e \(y\) son sumas de dos cuadrados, entonces \(xy\) también lo es

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

import Mathlib.Tactic
variable {α : Type _} [CommRing α]
variable {x y : α}

-- (suma_de_cuadrados x) afirma que x se puede escribir como la suma
-- de dos cuadrados.
def suma_de_cuadrados (x : α) :=
  ∃ a b, x = a^2 + b^2

example
  (hx : suma_de_cuadrados x)
  (hy : suma_de_cuadrados y)
  : suma_de_cuadrados (x * y) :=
by sorry