Demostrar que para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import data.real.basic open function variable {c : ℝ} example (h : c ≠ 0) : injective (λ x, c * x) := sorry |
Read More «Para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva»
Demostrar que para todo c ∈ ℝ, la función f(x) = x+c es inyectiva.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import data.real.basic open function variable {c : ℝ} example : injective (λ x, x + c) := sorry |
Read More «Para todo c ∈ ℝ, la función f(x) = x+c es inyectiva»
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:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
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 |
Read More «Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s»
Demostrar que si r ⊆ s y s ⊆ t, entonces r ⊆ t.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import tactic variables {α : Type*} variables r s t : set α example (rs : r ⊆ s) (st : s ⊆ t) : r ⊆ t := sorry |
Demostrar que, para cualquier conjunto s, s ⊆ s
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 |
import tactic variables {α : Type*} (s : set α) example : s ⊆ s := sorry |
La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x) y es impar si, para todo x, f(-x) -f(x).
Demostrar que si f es par y g es impar, entonces f ∘ g es par.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import data.real.basic variables (f g : ℝ → ℝ) def par (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) def impar (f : ℝ → ℝ) : Prop := ∀ x, f x = -f (-x) example (hf : par f) (hg : impar g) : par (f ∘ g) := sorry |
La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x) y es impar si, para todo x, f(-x) -f(x).
Demostrar que el producto de una función par por una impar es impar.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import data.real.basic variables (f g : ℝ → ℝ) def par (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) def impar (f : ℝ → ℝ) : Prop := ∀ x, f x = -f (-x) example (hf : par f) (hg : impar g) : impar (f * g) := sorry |
Read More «El producto de una función par por una impar es impar»
La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x) y es impar si, para todo x, f(-x) -f(x).
Demostrar que el producto de dos funciones impares es par.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import data.real.basic variables (f g : ℝ → ℝ) def par (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) def impar (f : ℝ → ℝ) : Prop := ∀ x, f x = -f (-x) example (hf : impar f) (hg : impar g) : par (f * g) := sorry |
La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x).
Demostrar que la suma de dos funciones pares es par.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import data.real.basic variables (f g : ℝ → ℝ) def par (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) example (hf : par f) (hg : par g) : par (f + g) := sorry |
Demostrar que la composición de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import data.real.basic variables (f g : ℝ → ℝ) example (mf : monotone f) (mg : monotone g) : monotone (f ∘ g) := sorry |
Read More «La composición de dos funciones monótonas es monótona»