{"id":2364,"date":"2024-04-06T11:25:00","date_gmt":"2024-04-06T09:25:00","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=2364"},"modified":"2024-04-06T11:25:00","modified_gmt":"2024-04-06T09:25:00","slug":"06-abr-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/06-abr-24\/","title":{"rendered":"f\u207b\u00b9[A \u222a B] = f\u207b\u00b9[A] \u222a f\u207b\u00b9[B]"},"content":{"rendered":"\n

Demostrar con Lean4 que \(f\u207b\u00b9[A \u222a B] = f\u207b\u00b9[A] \u222a f\u207b\u00b9[B]\).<\/p>\n

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

\nimport Mathlib.Data.Set.Function\n\nopen Set\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (A B : Set \u03b2)\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\nby sorry\n<\/pre>\n
<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Tenemos que demostrar que, para todo \(x\),
\n\[ x \u2208 f\u207b\u00b9[A \u222a B] \u2194 x \u2208 f\u207b\u00b9[A] \u222a f\u207b\u00b9[B] \]
\nLo haremos demostrando las dos implicaciones.<\/p>\n
(\u27f9) Supongamos que \(x \u2208 f\u207b\u00b9[A \u222a B]\). Entonces, \(f(x) \u2208 A \u222a B\).
\nDistinguimos dos casos:<\/p>\n
Caso 1: Supongamos que \(f(x) \u2208 A\). Entonces, \(x \u2208 f\u207b\u00b9[A]\) y, por tanto,
\n\(x \u2208 f\u207b\u00b9[A] \u222a f\u207b\u00b9[B]\).<\/p>\n
Caso 2: Supongamos que \(f(x) \u2208 B\). Entonces, \(x \u2208 f\u207b\u00b9[B]\) y, por tanto,
\n\(x \u2208 f\u207b\u00b9[A] \u222a f\u207b\u00b9[B]\).<\/p>\n
(\u27f8) Supongamos que \(x \u2208 f\u207b\u00b9[A] \u222a f\u207b\u00b9[B]\). Distinguimos dos casos.<\/p>\n
Caso 1: Supongamos que \(x \u2208 f\u207b\u00b9[A]\). Entonces, \(f(x) \u2208 A\) y, por tanto,
\n\(f(x) \u2208 A \u222a B\). Luego, \(x \u2208 f\u207b\u00b9[A \u222a B]\).<\/p>\n
Caso 2: Supongamos que \(x \u2208 f\u207b\u00b9[B]\). Entonces, \(f(x) \u2208 B\) y, por tanto,
\n\(f(x) \u2208 A \u222a B\). Luego, \(x \u2208 f\u207b\u00b9[A \u222a B]\).<\/p>\n
2. Demostraciones con Lean4<\/h2>\n
\nimport Mathlib.Data.Set.Function\n\nopen Set\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (A B : Set \u03b2)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\nby\n  ext x\n  -- x : \u03b1\n  -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B) \u2194 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n  constructor\n  . -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B) \u2192 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n    intro h\n    -- h : x \u2208 f \u207b\u00b9' (A \u222a B)\n    -- \u22a2 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n    rw [mem_preimage] at h\n    -- h : f x \u2208 A \u222a B\n    rcases h with fxA | fxB\n    . -- fxA : f x \u2208 A\n      left\n      -- \u22a2 x \u2208 f \u207b\u00b9' A\n      apply mem_preimage.mpr\n      -- \u22a2 f x \u2208 A\n      exact fxA\n    . -- fxB : f x \u2208 B\n      right\n      -- \u22a2 x \u2208 f \u207b\u00b9' B\n      apply mem_preimage.mpr\n      -- \u22a2 f x \u2208 B\n      exact fxB\n  . -- \u22a2 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B \u2192 x \u2208 f \u207b\u00b9' (A \u222a B)\n    intro h\n    -- h : x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n    -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B)\n    rw [mem_preimage]\n    -- \u22a2 f x \u2208 A \u222a B\n    rcases h with xfA | xfB\n    . -- xfA : x \u2208 f \u207b\u00b9' A\n      rw [mem_preimage] at xfA\n      -- xfA : f x \u2208 A\n      left\n      -- \u22a2 f x \u2208 A\n      exact xfA\n    . -- xfB : x \u2208 f \u207b\u00b9' B\n      rw [mem_preimage] at xfB\n      -- xfB : f x \u2208 B\n      right\n      -- \u22a2 f x \u2208 B\n      exact xfB\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\nby\n  ext x\n  -- x : \u03b1\n  -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B) \u2194 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n  constructor\n  . -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B) \u2192 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n    intros h\n    -- h : x \u2208 f \u207b\u00b9' (A \u222a B)\n    -- \u22a2 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n    rcases h with fxA | fxB\n    . -- fxA : f x \u2208 A\n      left\n      -- \u22a2 x \u2208 f \u207b\u00b9' A\n      exact fxA\n    . -- fxB : f x \u2208 B\n      right\n      -- \u22a2 x \u2208 f \u207b\u00b9' B\n      exact fxB\n  . -- \u22a2 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B \u2192 x \u2208 f \u207b\u00b9' (A \u222a B)\n    intro h\n    -- h : x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n    -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B)\n    rcases h with xfA | xfB\n    . -- xfA : x \u2208 f \u207b\u00b9' A\n      left\n      -- \u22a2 f x \u2208 A\n      exact xfA\n    . -- xfB : x \u2208 f \u207b\u00b9' B\n      right\n      -- \u22a2 f x \u2208 B\n      exact xfB\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\nby\n  ext x\n  -- x : \u03b1\n  -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B) \u2194 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n  constructor\n  . -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B) \u2192 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n    rintro (fxA | fxB)\n    . -- fxA : f x \u2208 A\n      -- \u22a2 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n      exact Or.inl fxA\n    . -- fxB : f x \u2208 B\n      -- \u22a2 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n      exact Or.inr fxB\n  . -- \u22a2 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B \u2192 x \u2208 f \u207b\u00b9' (A \u222a B)\n    rintro (xfA | xfB)\n    . -- xfA : x \u2208 f \u207b\u00b9' A\n      -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B)\n      exact Or.inl xfA\n    . -- xfB : x \u2208 f \u207b\u00b9' B\n      -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B)\n      exact Or.inr xfB\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\nby\n  ext x\n  -- x : \u03b1\n  -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B) \u2194 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n  constructor\n  . -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B) \u2192 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n    aesop\n  . -- \u22a2 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B \u2192 x \u2208 f \u207b\u00b9' (A \u222a B)\n    aesop\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\nby\n  ext x\n  -- x : \u03b1\n  -- \u22a2 x \u2208 f \u207b\u00b9' (A \u222a B) \u2194 x \u2208 f \u207b\u00b9' A \u222a f \u207b\u00b9' B\n  aesop\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\nby ext ; aesop\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\nby ext ; rfl\n\n-- 8\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\nrfl\n\n-- 9\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\npreimage_union\n\n-- 10\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B :=\nby simp\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (p q : Prop)\n-- #check (Or.inl: p \u2192 p \u2228 q)\n-- #check (Or.inr: q \u2192 p \u2228 q)\n-- #check (mem_preimage : x \u2208 f \u207b\u00b9' A \u2194 f x \u2208 A)\n-- #check (preimage_union : f \u207b\u00b9' (A \u222a B) = f \u207b\u00b9' A \u222a f \u207b\u00b9' B)\n<\/pre>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
3. Demostraciones con Isabelle\/HOL<\/h2>\n
\ntheory Imagen_inversa_de_la_union\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (u \u222a v) = f -` u \u222a f -` v\"\nproof (rule equalityI)\n  show \"f -` (u \u222a v) \u2286 f -` u \u222a f -` v\"\n  proof (rule subsetI)\n    fix x\n    assume \"x \u2208 f -` (u \u222a v)\"\n    then have \"f x \u2208 u \u222a v\"\n      by (rule vimageD)\n    then show \"x \u2208 f -` u \u222a f -` v\"\n    proof (rule UnE)\n      assume \"f x \u2208 u\"\n      then have \"x \u2208 f -` u\"\n        by (rule vimageI2)\n      then show \"x \u2208 f -` u \u222a f -` v\"\n        by (rule UnI1)\n    next\n      assume \"f x \u2208 v\"\n      then have \"x \u2208 f -` v\"\n        by (rule vimageI2)\n      then show \"x \u2208 f -` u \u222a f -` v\"\n        by (rule UnI2)\n    qed\n  qed\nnext\n  show \"f -` u \u222a f -` v \u2286 f -` (u \u222a v)\"\n  proof (rule subsetI)\n    fix x\n    assume \"x \u2208 f -` u \u222a f -` v\"\n    then show \"x \u2208 f -` (u \u222a v)\"\n    proof (rule UnE)\n      assume \"x \u2208 f -` u\"\n      then have \"f x \u2208 u\"\n        by (rule vimageD)\n      then have \"f x \u2208 u \u222a v\"\n        by (rule UnI1)\n      then show \"x \u2208 f -` (u \u222a v)\"\n        by (rule vimageI2)\n    next\n      assume \"x \u2208 f -` v\"\n      then have \"f x \u2208 v\"\n        by (rule vimageD)\n      then have \"f x \u2208 u \u222a v\"\n        by (rule UnI2)\n      then show \"x \u2208 f -` (u \u222a v)\"\n        by (rule vimageI2)\n    qed\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (u \u222a v) = f -` u \u222a f -` v\"\nproof\n  show \"f -` (u \u222a v) \u2286 f -` u \u222a f -` v\"\n  proof\n    fix x\n    assume \"x \u2208 f -` (u \u222a v)\"\n    then have \"f x \u2208 u \u222a v\" by simp\n    then show \"x \u2208 f -` u \u222a f -` v\"\n    proof\n      assume \"f x \u2208 u\"\n      then have \"x \u2208 f -` u\" by simp\n      then show \"x \u2208 f -` u \u222a f -` v\" by simp\n    next\n      assume \"f x \u2208 v\"\n      then have \"x \u2208 f -` v\" by simp\n      then show \"x \u2208 f -` u \u222a f -` v\" by simp\n    qed\n  qed\nnext\n  show \"f -` u \u222a f -` v \u2286 f -` (u \u222a v)\"\n  proof\n    fix x\n    assume \"x \u2208 f -` u \u222a f -` v\"\n    then show \"x \u2208 f -` (u \u222a v)\"\n    proof\n      assume \"x \u2208 f -` u\"\n      then have \"f x \u2208 u\" by simp\n      then have \"f x \u2208 u \u222a v\" by simp\n      then show \"x \u2208 f -` (u \u222a v)\" by simp\n    next\n      assume \"x \u2208 f -` v\"\n      then have \"f x \u2208 v\" by simp\n      then have \"f x \u2208 u \u222a v\" by simp\n      then show \"x \u2208 f -` (u \u222a v)\" by simp\n    qed\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (u \u222a v) = f -` u \u222a f -` v\"\n  by (simp only: vimage_Un)\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (u \u222a v) = f -` u \u222a f -` v\"\n  by auto\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"
Demostrar con Lean4 que \(f\u207b\u00b9[A \u222a B] = f\u207b\u00b9[A] \u222a f\u207b\u00b9[B]\). Para ello, completar la siguiente teor\u00eda de Lean4: import Mathlib.Data.Set.Function open Set variable {\u03b1 \u03b2 : Type _} variable (f : \u03b1 \u2192 \u03b2) variable (A B : Set \u03b2) example : f \u207b\u00b9’ (A \u222a B) = f \u207b\u00b9’ A \u222a f \u207b\u00b9’ B := by sorry<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"default","_kad_post_title":"default","_kad_post_layout":"default","_kad_post_sidebar_id":"","_kad_post_content_style":"default","_kad_post_vertical_padding":"default","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[17],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2364"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=2364"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2364\/revisions"}],"predecessor-version":[{"id":2365,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2364\/revisions\/2365"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=2364"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=2364"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=2364"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}