Demostrar con Lean4 que la suma de dos funciones acotadas inferiormente también lo está.
Para ello, completar la siguiente teoría de Lean4:
import src.Suma_de_cotas_inferiores variable {f g : ℝ → ℝ} -- (acotadaInf f) afirma que f tiene cota inferior. def acotadaInf (f : ℝ → ℝ) := ∃ a, CotaInferior f a example (hf : acotadaInf f) (hg : acotadaInf g) : acotadaInf (f + g) := by sorry
Demostrar con Lean4 que la suma de dos funciones acotadas superiormente también lo está.
Para ello, completar la siguiente teoría de Lean4:
import src.Suma_de_cotas_superiores variable {f g : ℝ → ℝ} -- (acotadaSup f) afirma que f tiene cota superior. def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a example (hf : acotadaSup f) (hg : acotadaSup g) : acotadaSup (f + g) := by sorry
Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx\) es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic open Function variable {c : ℝ} example (h : c ≠ 0) : Injective ((c * .)) := by sorry
Demostrar con Lean4 que la función \(x ↦ x + c\) es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic open Function variable {c : ℝ} example : Injective ((. + c)) := by sorry
Demostrar con Lean4 que si \(f\) es par y \(g\) es impar, entonces \(f ∘ g\) es par.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) example (h1 : esPar f) (h2 : esImpar g) : esPar (f ∘ g) := by sorry
Demostrar con Lean4 que el producto de una función par por una impar es impar.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) example (h1 : esPar f) (h2 : esImpar g) : esImpar (f * g) := by sorry
Demostrar con Lean4 que el producto de dos funciones impares es par.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) example (h1 : esImpar f) (h2 : esImpar g) : esPar (f * g) := by sorry
Demostrar con Lean4 que la suma de dos funciones pares es par.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) example (h1 : esPar f) (h2 : esPar g) : esPar (f + g) := by sorry
Demostrar con Lean4 que la composición de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) example (mf : Monotone f) (mg : Monotone g) : Monotone (f ∘ g) := by sorry
Demostrar con Lean4 que si \(c\) es no negativo y \(f\) es monótona, entonces \(cf\) es monótona.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable {c : ℝ} example (mf : Monotone f) (nnc : 0 ≤ c) : Monotone (fun x ↦ c * f x) := by sorry