Menu Close

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

José A. Alonso-

Demostrar que si x e y son sumas de dos cuadrados, entonces xy también lo es.

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

import tactic
variables {α : Type*} [comm_ring α]
variables {x y : α}
 
-- (es_suma_de_cuadrados x) se verifica si x se puede escribir como la
-- suma de dos cuadrados.
def es_suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2
 
example
  (hx : es_suma_de_cuadrados x)
  (hy : es_suma_de_cuadrados y)
  : es_suma_de_cuadrados (x * y) :=
sorry
Soluciones →

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

José A. Alonso-

Demostrar que si c ≥ 0 y f está acotada superiormente, entonces c * f también lo está.

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

import data.real.basic
 
variables {f : ℝ → ℝ}                    
variables {a c : ℝ}                      
 
-- (cota_superior f a) se verifica si a es una cota superior de f.
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a
 
-- (acotada_sup f) se verifica si f tiene cota superior.
def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a
 
example
  (hf : acotada_sup f)
  (h : c ≥ 0)
  : acotada_sup (λ x, c * f x) :=
sorry
Soluciones →

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

José A. Alonso-

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

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

import data.real.basic
 
variables {f g : ℝ → ℝ}
variables {a b : ℝ}
 
-- (cota_inferior f a) se verifica si a es una cota inferior de f.
def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x
 
-- (acotada_inf f) se verifica si f tiene cota inferior.
def acotada_inf (f : ℝ → ℝ) := ∃ a, cota_inferior f a
 
example
  (hf : acotada_inf f)
  (hg : acotada_inf g)
  : acotada_inf (f + g) :=
sorry
Soluciones →

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

José A. Alonso-

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

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

import data.real.basic
 
variables {f g : ℝ → ℝ}
variables {a b : ℝ}
 
-- (cota_superior f a) se verifica si a es una cota superior de f.
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a
 
-- (acotada_sup f) afirma que f tiene cota superior.
def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a
 
example
  (hf : acotada_sup f)
  (hg : acotada_sup g)
  : acotada_sup (f + g) :=
sorry
Soluciones →

Si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva

José A. Alonso-

Demostrar que si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva.

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

import tactic
 
open function
 
variables {A : Type*} {B : Type*} {C : Type*}
variables {f : A → B} {g : B → C}
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g ∘ f) :=
sorry
Soluciones →