{"id":1894,"date":"2024-01-01T06:00:44","date_gmt":"2024-01-01T04:00:44","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1894"},"modified":"2023-12-29T13:57:02","modified_gmt":"2023-12-29T11:57:02","slug":"01-ene-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/01-ene-24\/","title":{"rendered":"f: \u211d \u2192 \u211d no es mon\u00f3tona syss (\u2203x,y)[x \u2264 y \u2227 f(x) > f(y)]\u200b"},"content":{"rendered":"\n

Demostrar con Lean4 que \(f: \u211d \u2192 \u211d\) no es mon\u00f3tona syss \((\u2203x,y)[x \u2264 y \u2227 f(x) > f(y)]\)\u200b.<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\nimport Mathlib.Data.Real.Basic\nvariable {f : \u211d \u2192 \u211d}\n\nexample :\n  \u00acMonotone f \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y :=\nsorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Por la siguiente cadena de equivalencias:
\n\begin{align}
\n   f \text{ es no mon\u00f3tona } & \u2194 \u00ac(\u2200 x, y)[x \u2264 y \u2192 f(x) \u2264 f(y)] \\
\n                             & \u2194 (\u2203 x, y)[x \u2264 y \u2227 f(x) > f(y)]
\n\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable {f : \u211d \u2192 \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  \u00acMonotone f \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y :=\ncalc\n  \u00acMonotone f\n    \u2194 \u00ac\u2200 x y, x \u2264 y \u2192 f x \u2264 f y := by rw [Monotone]\n  _ \u2194 \u2203 x y, x \u2264 y \u2227 f y < f x  := by simp_all only [not_forall, not_le, exists_prop]\n  _ \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y  := by rfl\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  \u00acMonotone f \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y :=\ncalc\n  \u00acMonotone f\n    \u2194 \u00ac\u2200 x y, x \u2264 y \u2192 f x \u2264 f y := by rw [Monotone]\n  _ \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y  := by aesop\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  \u00acMonotone f \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y :=\nby\n  rw [Monotone]\n  -- \u22a2 (\u00ac\u2200 \u2983a b : \u211d\u2984, a \u2264 b \u2192 f a \u2264 f b) \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y\n  push_neg\n  -- \u22a2 (Exists fun \u2983a\u2984 => Exists fun \u2983b\u2984 => a \u2264 b \u2227 f b < f a) \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y\n  rfl\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nlemma not_Monotone_iff :\n  \u00acMonotone f \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y :=\nby\n  rw [Monotone]\n  -- \u22a2 (\u00ac\u2200 \u2983a b : \u211d\u2984, a \u2264 b \u2192 f a \u2264 f b) \u2194 \u2203 x y, x \u2264 y \u2227 f x > f y\n  aesop\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n