noviembre 2023 – Página 2

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

PorJosé A. Alonso 16 noviembre 20237 noviembre 2023

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

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

import Mathlib.Data.Real.Basic

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)

PorJosé A. Alonso 15 noviembre 20235 noviembre 2023

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

import Mathlib.Data.Real.Basic

variable (a b : ℝ)

example

(h : a < b)

: ¬ b < a :=

by sorry

Read More «En ℝ, a < b → ¬(b < a)"

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