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»
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 |
Demostrar que (s \ t) \ u ⊆ s \ (t ∪ u)
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import data.set.basic open set variable {α : Type} variables s t u : set α example : (s \ t) \ u ⊆ s \ (t ∪ u) := sorry |