Para cualquier conjunto s, s ⊆ s
Demostrar con Lean4 que para cualquier conjunto \(s\), \(s ⊆ s\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {α : Type _} variable (s : Set α) example : s ⊆ s := by sorry
Si f es par y g es impar, entonces (f ∘ g) es par
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
El producto de una función par por una impar es impar
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
El producto de dos funciones impares es par
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
La suma de dos funciones pares es par
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
La composición de dos funciones monótonas es monótona
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
Si c es no negativo y f es monótona, entonces cf es monótona.
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
La suma de dos funciones monótonas es monótona
Demostrar con Lean4 que la suma 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
Si a es una cota superior no negativa de f y b es una cota superior de la función no negativa g, entonces ab es una cota superior de fg
Sean \(f\) y \(g\) funciones de \(ℝ\) en \(ℝ\). Demostrar con Lean4 que si \(a\) es una cota superior no negativa de \(f\) y \(b\) es es una cota superior de la función no negativa \(g\), entonces \(ab\) es una cota superior de \(fg\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic -- (CotaSuperior f a) se verifica si a es una cota superior de f. def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) variable (a b : ℝ) example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) (nng : CotaInferior g 0) (nna : 0 ≤ a) : CotaSuperior (f * g) (a * b) := by sorry
El producto de funciones no negativas es no negativo
Demostrar con Lean4 que si \(f\) y \(g\) son funciones no negativas de \(ℝ\) en \(ℝ\), entonces su producto es no negativo.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) example (nnf : CotaInferior f 0) (nng : CotaInferior g 0) : CotaInferior (f * g) 0 := by sorry