{"id":1835,"date":"2023-12-07T06:00:09","date_gmt":"2023-12-07T04:00:09","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1835"},"modified":"2023-11-27T15:08:12","modified_gmt":"2023-11-27T13:08:12","slug":"07-dic-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/07-dic-23\/","title":{"rendered":"Si f no es mon\u00f3tona, entonces \u2203x\u2203y[x \u2264 y \u2227 f(y) < f(x)]\u200b"},"content":{"rendered":"\n

Demostrar con Lean4 que si \(f\) no es mon\u00f3tona, entonces \(\u2203x\u2203y[x \u2264 y \u2227 f(y) < f(x)]\u200b\).<\/p>\n

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

\nimport Mathlib.Tactic\nvariable (f : \u211d \u2192 \u211d)\n\nexample\n  (h : \u00acMonotone f)\n  : \u2203 x y, x \u2264 y \u2227 f y < f x :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Usaremos los siguientes lemas:
\n\begin{align}
\n   &\u00ac(\u2200x)P(x) \u2194 (\u2203 x)\u00acP(x)      \tag{L1} \\
\n   &\u00ac(p \u2192 q) \u2194 p \u2227 \u00acq           \tag{L2} \\
\n   &(\u2200a, b \u2208 \u211d)[\u00acb \u2264 a \u2192 a < b] \tag{L3}
\n\end{align}<\/p>\n
Por la definici\u00f3n de funci\u00f3n mon\u00f3tona,
\n\[ \u00ac(\u2200x)(\u2200y)[x \u2264 y \u2192 f(x) \u2264 f(y)] \]
\nAplicando L1 se tiene
\n\[ (\u2203x)\u00ac(\u2200y)[x \u2264 y \u2192 f(x) \u2264 f(y)] \]
\nSea \(a\) tal que
\n\[ \u00ac(\u2200y)[a \u2264 y \u2192 f(a) \u2264 f(y)] \]
\nAplicando L1 se tiene
\n\[ (\u2203y)\u00ac[a \u2264 y \u2192 f(a) \u2264 f(y)] \]
\nSea \(b\) tal que
\n\[ \u00ac[a \u2264 b \u2192 f(a) \u2264 f(b)] \]
\nAplicando L2 se tiene que
\n\[ a \u2264 b \u2227 \u00ac(f(a) \u2264 f(b)) \]
\nAplicando L3 se tiene que
\n\[ a \u2264 b \u2227 f(b) < f(a) \]
\nPor tanto,
\n\[ (\u2203x,y)[x \u2264 y \u2227 f(y) < f(x)] \]<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Tactic\nvariable (f : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00acMonotone f)\n  : \u2203 x y, x \u2264 y \u2227 f y < f x :=\nby\n  have h1 : \u00ac\u2200 x y, x \u2264 y \u2192 f x \u2264 f y := h\n  have h2 : \u2203 x, \u00ac(\u2200 y, x \u2264 y \u2192 f x \u2264 f y) := not_forall.mp h1\n  rcases h2 with \u27e8a, ha : \u00ac\u2200 y, a \u2264 y \u2192 f a \u2264 f y\u27e9\n  have h3 : \u2203 y, \u00ac(a \u2264 y \u2192 f a \u2264 f y) := not_forall.mp ha\n  rcases h3 with \u27e8b, hb : \u00ac(a \u2264 b \u2192 f a \u2264 f b)\u27e9\n  have h4 : a \u2264 b \u2227 \u00ac(f a \u2264 f b) := not_imp.mp hb\n  have h5 : a \u2264 b \u2227 f b < f a := \u27e8h4.1, lt_of_not_le h4.2\u27e9\n  use a, b\n  -- \u22a2 a \u2264 b \u2227 f b < f a\n  exact h5\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00acMonotone f)\n  : \u2203 x y, x \u2264 y \u2227 f y < f x :=\nby\n  simp only [Monotone] at h\n  -- h : \u00ac\u2200 \u2983a b : \u211d\u2984, a \u2264 b \u2192 f a \u2264 f b\n  push_neg at h\n  -- h : Exists fun \u2983a\u2984 => Exists fun \u2983b\u2984 => a \u2264 b \u2227 f b < f a\n  exact h\n\n-- Lemas usados\n-- ============\n\n-- variable {\u03b1 : Type _}\n-- variable (P : \u03b1 \u2192 Prop)\n-- variable (p q : Prop)\n-- variable (a b : \u211d)\n-- #check (not_forall : (\u00ac\u2200 x, P x) \u2194 \u2203 x, \u00acP x)\n-- #check (not_imp : \u00ac(p \u2192 q) \u2194 p \u2227 \u00acq)\n-- #check (lt_of_not_le : \u00acb \u2264 a \u2192 a < b)\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