Demostrar que si a, b, c, d, e y f son números reales tales que
|
1 2 |
a * b = c * d e = f |
Entonces,
|
1 |
a * (b * e) = c * (d * f) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import data.real.basic variables a b c d e f : ℝ example (h1 : a * b = c * d) (h2 : e = f) : a * (b * e) = c * (d * f) := |
Demostrar que los números reales tienen la siguiente propiedad
|
1 |
(a * b) * c = b * (a * c) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import data.real.basic variables a b c : ℝ example : (a * b) * c = b * (a * c) := sorry |
Read More «Si a, b y c son números reales, entonces (a * b) * c = b * (a * c)»
Demostrar que los productos de los números naturales por números pares son pares.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import data.nat.parity import tactic open nat example : ∀ m n : ℕ, even n → even (m * n) := sorry |
Demostrar que si f·f es biyectiva, entonces f es biyectiva.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import tactic open function variable {X: Type} example (f : X → X) (Hff : bijective (f ∘ f)) : bijective f := sorry |
Demostrar que si g·f es suprayectiva, entonces g es suprayectiva.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import tactic open function variables {X Y Z : Type} variable {f : X → Y} variable {g : Y → Z} example (Hgf : surjective (g ∘ f)) : surjective g := sorry |
Read More «Si g·f es suprayectiva, entonces g es suprayectiva»
Demostrar que si g·f es inyectiva, entonces f es inyectiva.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import tactic open function variables {X Y Z : Type} variable {f : X → Y} variable {g : Y → Z} example (Hgf : injective (g ∘ f)) : injective f := sorry |
Demostrar el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en su conjunto potencia.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import data.set.basic open function variables {α : Type} example : ∀ f : α → set α, ¬ surjective f := sorry |
En Lean, la imagen de un conjunto s por una función f se representa por f '' s; es decir, f '' s = {y | ∃ x, x ∈ s ∧ f x = y}
Demostrar que f '' (s ∪ t) = f '' s ∪ f '' t
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import data.set.basic import tactic open set variables {α : Type*} {β : Type*} variable f : α → β variables s t : set α example : f '' (s ∪ t) = f '' s ∪ f '' t := sorry |
En Lean, la imagen inversa de un conjunto s (de elementos de tipo por la función f (de tipo α → β) es el conjunto f ⁻¹' s de elementos x (de tipo α) tales que f x ∈ s.
Demostrar que f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import data.set.basic open set variables {α : Type*} {β : Type*} variable f : α → β variables u v : set β example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := sorry |
Demostrar que s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s)
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import data.set.basic import data.set.lattice import tactic open set variable {α : Type} variable s : set α variable A : ℕ → set α example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) := sorry |
Read More «Distributiva de la intersección respecto de la unión general»