Menu Close

Mes: noviembre 2022

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

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

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

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

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

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

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

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

Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s

Demostrar que si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s

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

import tactic
 
variables {α : Type*} [partial_order α]
variables s : set α
variables a b : α
 
-- (cota_superior s a) expresa que a es una cota superior de s.
def cota_superior (s : set α) (a : α) :=  {x}, x ∈ s  x  a
 
example
  (h1 : cota_superior s a)
  (h2 : a  b)
  : cota_superior s b :=
sorry

Si r ⊆ s y s ⊆ t, entonces r ⊆ t

Demostrar que si r ⊆ s y s ⊆ t, entonces r ⊆ t.

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

import tactic
 
variables {α : Type*}
variables r s t : set α
 
example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
sorry