José A. Alonso

La composición de funciones suprayectivas es suprayectiva

PorJosé A. Alonso 14 noviembre 20233 noviembre 2023

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

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 suprayectiva, entonces ∃x ∈ ℝ tal que f(x)² = 9

PorJosé A. Alonso 13 noviembre 20232 noviembre 2023

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
open Function

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

import Mathlib.Data.Real.Basic

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

PorJosé A. Alonso 10 noviembre 202311 noviembre 2023

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

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

PorJosé A. Alonso 9 noviembre 202330 octubre 2023

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

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

PorJosé A. Alonso 8 noviembre 202330 octubre 2023

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
variable {c : ℝ}
open Function

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

import Mathlib.Data.Real.Basic

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

PorJosé A. Alonso 7 noviembre 20237 noviembre 2023

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

import Mathlib.Tactic

variable {a b c : ℕ}

example

(h1 : a ∣ b)

(h2 : a ∣ c)

: a ∣ (b + c) :=

by sorry

Transitividad de la divisibilidad

PorJosé A. Alonso 6 noviembre 202329 octubre 2023

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

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

PorJosé A. Alonso 3 noviembre 202326 octubre 2023

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

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

Si c ≥ 0 y f está acotada superiormente, entonces c·f también lo está

PorJosé A. Alonso 2 noviembre 202326 octubre 2023

Demostrar con Lean4 que si \(c ≥ 0\) y \(f\) está acotada superiormente, entonces \(c·f\) también lo está.

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

import src.Cota_superior_de_producto_por_escalar

variable {f : ℝ → ℝ}
variable {c : ℝ}

-- (acotadaSup f) afirma que f tiene cota superior.
def acotadaSup (f : ℝ → ℝ) :=
  ∃ a, CotaSuperior f a

example
  (hf : acotadaSup f)
  (hc : c ≥ 0)
  : acotadaSup (fun x ↦ c * f x) :=
by sorry

import src.Cota_superior_de_producto_por_escalar

variable {f : ℝ → ℝ}

variable {c : ℝ}

-- (acotadaSup f) afirma que f tiene cota superior.

def acotadaSup (f : ℝ → ℝ) :=

∃ a, CotaSuperior f a

example

(hf : acotadaSup f)

(hc : c ≥ 0)

: acotadaSup (fun x ↦ c * f x) :=

by sorry

Si a es una cota superior de f y c ≥ 0, entonces ca es una cota superior de cf

PorJosé A. Alonso 1 noviembre 202326 octubre 2023

Demostrar con Lean4 que si \(a\) es una cota superior de \(f\) y \(c ≥ 0\), entonces \(ca\) es una cota superior de \(cf\).

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

import Mathlib.Data.Real.Basic

-- (CotaSuperior f a) se verifica si a es una cota superior de f.
def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

variable {f : ℝ → ℝ}
variable {c : ℝ}

example
  (hfa : CotaSuperior f a)
  (h : c ≥ 0)
  : CotaSuperior (fun x ↦ c * f x) (c * a) :=
by sorry

import Mathlib.Data.Real.Basic

-- (CotaSuperior f a) se verifica si a es una cota superior de f.

def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=

∀ x, f x ≤ a

variable {f : ℝ → ℝ}

variable {c : ℝ}

example

(hfa : CotaSuperior f a)

(h : c ≥ 0)

: CotaSuperior (fun x ↦ c * f x) (c * a) :=

by sorry