José A. AlonsoDemostrar que si a divide a b y a c, entonces también divide a b + c.
Para ello, completar la siguiente teoría de Lean:
import tactic variables {a b c : ℕ} example (divab : a ∣ b) (divac : a ∣ c) : a ∣ (b + c) := sorry |
Demostrar que la relación de divisibilidad es transitiva.
Para ello, completar la siguiente teoría de Lean:
import tactic variables {a b c : ℕ} example (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := sorry |
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 |
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 |
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 |
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 |
Demostrar que ∃ x ∈ ℝ, 2 < x < 3
Para ello, completar la siguiente teoría de Lean:
import data.real.basic example : ∃ x : ℝ, 2 < x ∧ x < 3 := sorry |
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 |
Demostrar que para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva
Para ello, completar la siguiente teoría de Lean:
import data.real.basic open function variable {c : ℝ} example (h : c ≠ 0) : injective (λ x, c * x) := sorry |
Demostrar que para todo c ∈ ℝ, la función f(x) = x+c es inyectiva.
Para ello, completar la siguiente teoría de Lean:
import data.real.basic open function variable {c : ℝ} example : injective (λ x, x + c) := sorry |