Sin categoría – Página 7

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

La suma de dos funciones acotadas inferiormente también lo está

PorJosé A. Alonso 31 octubre 202330 octubre 2023

Demostrar con Lean4 que la suma de dos funciones acotadas inferiormente también lo está.

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

import src.Suma_de_cotas_inferiores
variable {f g : ℝ → ℝ}

-- (acotadaInf f) afirma que f tiene cota inferior.
def acotadaInf (f : ℝ → ℝ) :=
  ∃ a, CotaInferior f a

example
  (hf : acotadaInf f)
  (hg : acotadaInf g)
  : acotadaInf (f + g) :=
by sorry

import src.Suma_de_cotas_inferiores

variable {f g : ℝ → ℝ}

-- (acotadaInf f) afirma que f tiene cota inferior.

def acotadaInf (f : ℝ → ℝ) :=

∃ a, CotaInferior f a

example

(hf : acotadaInf f)

(hg : acotadaInf g)

: acotadaInf (f + g) :=

by sorry

La suma de dos funciones acotadas superiormente también lo está

PorJosé A. Alonso 30 octubre 202323 octubre 2023

Demostrar con Lean4 que la suma de dos funciones acotadas superiormente también lo está.

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

import src.Suma_de_cotas_superiores
variable {f g : ℝ → ℝ}

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

example
  (hf : acotadaSup f)
  (hg : acotadaSup g)
  : acotadaSup (f + g) :=
by sorry

import src.Suma_de_cotas_superiores

variable {f g : ℝ → ℝ}

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

def acotadaSup (f : ℝ → ℝ) :=

∃ a, CotaSuperior f a

example

(hf : acotadaSup f)

(hg : acotadaSup g)

: acotadaSup (f + g) :=

by sorry

Hay algún número real entre 2 y 3

PorJosé A. Alonso 27 octubre 202319 octubre 2023

Demostrar con Lean4 que hay algún número real entre 2 y 3.

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

import Mathlib.Data.Real.Basic

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
by sorry

import Mathlib.Data.Real.Basic

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=

by sorry

La composición de funciones inyectivas es inyectiva

PorJosé A. Alonso 26 octubre 202319 octubre 2023

Demostrar con Lean4 que la composición de funciones inyectivas es inyectiva.

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

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

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

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}

variable {f : α → β} {g : β → γ}

example

(hg : Injective g)

(hf : Injective f) :

Injective (g ∘ f) :=

by sorry

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

PorJosé A. Alonso 25 octubre 202318 octubre 2023

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

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

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

example
  (h : c ≠ 0)
  : Injective ((c * .)) :=
by sorry

import Mathlib.Data.Real.Basic

open Function

variable {c : ℝ}

example

(h : c ≠ 0)

: Injective ((c * .)) :=

by sorry