Demostrar con Lean4 que si \(r ⊆ s\) y \(s ⊆ t\), entonces \(r ⊆ t\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Set variable {α : Type _} variable (r s t : Set α) example (rs : r ⊆ s) (st : s ⊆ t) : r ⊆ t := by sorry
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
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
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
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