Sea una funci\u00f3n f de \u211d en \u211d. Se dice que f es creciente si para todo x e y tales que x \u2264 y se tiene que f(x) \u2264 f(y). Se dice que f es decreciente si para todo x e y tales que x \u2264 y se tiene que f(x) \u2265 f(y).<\/p>\n
Demostrar que si f es creciente y g es decreciente, entonces (g \u2218 f) es decreciente.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.real.basic\n\nvariables (f g : \u211d \u2192 \u211d)\n\ndef creciente (f : \u211d \u2192 \u211d) : Prop :=\n\u2200 {x y}, x \u2264 y \u2192 f x \u2264 f y\n\ndef decreciente (f : \u211d \u2192 \u211d) : Prop :=\n\u2200 {x y}, x \u2264 y \u2192 f x \u2265 f y\n\nexample\n (hf : creciente f)\n (hg : decreciente g)\n : decreciente (g \u2218 f) :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport data.real.basic\r\n\r\nvariables (f g : \u211d \u2192 \u211d)\r\n\r\ndef creciente (f : \u211d \u2192 \u211d) : Prop :=\r\n\u2200 {x y}, x \u2264 y \u2192 f x \u2264 f y\r\n\r\ndef decreciente (f : \u211d \u2192 \u211d) : Prop :=\r\n\u2200 {x y}, x \u2264 y \u2192 f x \u2265 f y\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (hf : creciente f)\r\n (hg : decreciente g)\r\n : decreciente (g \u2218 f) :=\r\nbegin\r\n intros x y hxy,\r\n calc (g \u2218 f) x\r\n = g (f x) : rfl\r\n ... \u2265 g (f y) : hg (hf hxy)\r\n ... = (g \u2218 f) y : rfl,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n (hf : creciente f)\r\n (hg : decreciente g)\r\n : decreciente (g \u2218 f) :=\r\nbegin\r\n unfold creciente decreciente at *,\r\n intros x y h,\r\n unfold function.comp,\r\n apply hg,\r\n apply hf,\r\n exact h,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n (hf : creciente f)\r\n (hg : decreciente g)\r\n : decreciente (g \u2218 f) :=\r\nbegin\r\n intros x y h,\r\n apply hg,\r\n apply hf,\r\n exact h,\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n (hf : creciente f)\r\n (hg : decreciente g)\r\n : decreciente (g \u2218 f) :=\r\nbegin\r\n intros x y h,\r\n apply hg,\r\n exact hf h,\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample\r\n (hf : creciente f)\r\n (hg : decreciente g)\r\n : decreciente (g \u2218 f) :=\r\nbegin\r\n intros x y h,\r\n exact hg (hf h),\r\nend\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample\r\n (hf : creciente f)\r\n (hg : decreciente g)\r\n : decreciente (g \u2218 f) :=\r\n\u03bb x y h, hg (hf h)\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample\r\n (hf : creciente f)\r\n (hg : decreciente g)\r\n : decreciente (g \u2218 f) :=\r\nassume x y,\r\nassume h : x \u2264 y,\r\nhave h1 : f x \u2264 f y,\r\n from hf h,\r\nshow (g \u2218 f) x \u2265 (g \u2218 f) y,\r\n from hg h1\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\nexample\r\n (hf : creciente f)\r\n (hg : decreciente g)\r\n : decreciente (g \u2218 f) :=\r\nassume x y,\r\nassume h : x \u2264 y,\r\nshow (g \u2218 f) x \u2265 (g \u2218 f) y,\r\n from hg (hf h)\r\n\r\n-- 9\u00aa demostraci\u00f3n\r\nexample\r\n (hf : creciente f)\r\n (hg : decreciente g)\r\n : decreciente (g \u2218 f) :=\r\n\u03bb x y h, hg (hf h)\r\n\r\n-- 10\u00aa demostraci\u00f3n\r\nexample\r\n (hf : creciente f)\r\n (hg : decreciente g)\r\n : decreciente (g \u2218 f) :=\r\n-- by hint\r\nby tauto\r\n<\/pre>\n