Demostrar con Lean4 que la función \(x ↦ x + c\) es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable {c : ℝ} open Function example : Surjective (fun x ↦ x + c) := by sorry |
Demostrar con Lean4 que si \(a\) divide a \(b\) y a \(c\), entonces divide a \(b+c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Tactic variable {a b c : ℕ} example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by sorry |
Demostrar con Lean4 la transitividad de la divisibilidad.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Tactic variable {a b c : ℕ} example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by sorry |
Demostrar con Lean4 que si \(x\) e \(y\) son sumas de dos cuadrados, entonces \(xy\) también lo es
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Tactic variable {α : Type _} [CommRing α] variable {x y : α} -- (suma_de_cuadrados x) afirma que x se puede escribir como la suma -- de dos cuadrados. def suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2 example (hx : suma_de_cuadrados x) (hy : suma_de_cuadrados y) : suma_de_cuadrados (x * y) := by sorry |
Read More «Si x e y son sumas de dos cuadrados, entonces xy también lo es»
Demostrar con Lean4 que si \(c ≥ 0\) y \(f\) está acotada superiormente, entonces \(c·f\) también lo está.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import src.Cota_superior_de_producto_por_escalar variable {f : ℝ → ℝ} variable {c : ℝ} -- (acotadaSup f) afirma que f tiene cota superior. def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a example (hf : acotadaSup f) (hc : c ≥ 0) : acotadaSup (fun x ↦ c * f x) := by sorry |
Read More «Si c ≥ 0 y f está acotada superiormente, entonces c·f también lo está»