Sean a, b y c números reales. Demostrar que
|
1 |
min (min a b) c = min a (min b c) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import data.real.basic tactic variables a b c : ℝ example : min (min a b) c = min a (min b c) := sorry |
Read More «Si a, b, c ∈ ℝ, entonces min(min(a,b),c) = min(a,min(b,c))»
Demostrar que si a, b ∈ ℝ, entonces max(a,b) = max(b,a)
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import data.real.basic variables a b : ℝ example : max a b = max b a := sorry |
Demostrar que si a, b ∈ ℝ, entonces min(a,b) = min(b,a).
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import data.real.basic variables a b : ℝ example : min a b = min b a := sorry |
Demostrar que si a, b ∈ ℝ, entonces |ab| ≤ (a² + b²)/2
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import data.real.basic import tactic variables a b : ℝ example : abs (a*b) ≤ (a^2 + b^2) / 2 := sorry |
Demostrar que si a, b ∈ ℝ, entonces 2ab ≤ a² + b²
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import data.real.basic import tactic variables a b : ℝ example : 2*a*b ≤ a^2 + b^2 := sorry |
Demostrar que si a, b, c ∈ ℝ tales que a ≤ b, entonces c – eᵇ ≤ c – eᵃ.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import analysis.special_functions.log.basic import tactic open real variables a b c : ℝ example (h : a ≤ b) : c - exp b ≤ c - exp a := sorry |
Read More «Si a, b, c ∈ ℝ tales que a ≤ b, entonces c – eᵇ ≤ c – eᵃ»
Demostrar que si a, b ∈ ℝ tales que a ≤ b, entonces log(1 + eᵃ) ≤ log(1 + eᵇ).
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import analysis.special_functions.log.basic open real variables a b : ℝ example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := sorry |
Read More «Si a, b ∈ ℝ tales que a ≤ b, entonces log(1 + eᵃ) ≤ log(1 + eᵇ)»
Demostrar que si a, b, c, d, f ∈ ℝ tales que
|
1 2 |
a ≤ b c < d |
entonces
|
1 |
a + eᶜ + f < b + eᵈ + f |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import analysis.special_functions.log.basic open real variables a b c d f : ℝ example (hab : a ≤ b) (hcd : c < d) : a + exp c + f < b + exp d + f := sorry |
Read More «Si a, b, c, d, f ∈ ℝ tales que a ≤ b y c < d, entonces a + eᶜ + f < b + eᵈ + f"
Demostrar que si a, b, d ∈ ℝ tales que 
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import analysis.special_functions.log.basic open real variables a b d : ℝ example (h : 1 ≤ a) (h' : b ≤ d) : 2 + a + exp b ≤ 3 * a + exp d := sorry |
Nota: Se pueden usar los lemas
|
1 2 |
add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d exp_le_exp : exp a ≤ exp b ↔ a ≤ b |
Read More «Si a, b, d ∈ ℝ tales que 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ»
Demostrar que si a, b, c, d, e ∈ ℝ tales que
|
1 2 3 4 |
a ≤ b b < c c ≤ d d < e |
entonces
|
1 |
a < e |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import data.real.basic variables a b c d e : ℝ example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := sorry |
Read More «Si a, b, c, d, e ∈ ℝ tales que a ≤ b, b < c, c ≤ d, d < e, entonces a < e"