La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g
Demostrar con Lean4 que si \(f\) y \(g\) son funciones de \(ℝ\) en \(ℝ\), entonces la suma de una cota inferior de \(f\) y una cota inferior de \(g\) es una cota inferior de \(f+g\).
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.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 : ℝ → ℝ) variable (a b : ℝ) example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := by sorry |
Read More «La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g»