José A. Alonso

Imagen de imagen inversa de aplicaciones suprayectivas

PorJosé A. Alonso 11 junio 202112 junio 2021

Demostrar que si f es suprayectiva, entonces

   u ⊆ f[f⁻¹[u]]

1	u ⊆ f[f⁻¹[u]]

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set function

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  u : set β

example
  (h : surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
sorry

import data.set.basic

open set function

variables {α : Type*} {β : Type*}

variable f : α → β

variable u : set β

example

(h : surjective f)

: u ⊆ f '' (f⁻¹' u) :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
open set function

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  u : set β

-- 1ª demostración
-- ===============

example
  (h : surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
begin
  intros y yu,
  cases h y with x fxy,
  use x,
  split,
  { apply mem_preimage.mpr,
    rw fxy,
    exact yu },
  { exact fxy },
end

-- 2ª demostración
-- ===============

example
  (h : surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
begin
  intros y yu,
  cases h y with x fxy,
  use x,
  split,
  { show f x ∈ u,
    rw fxy,
    exact yu },
  { exact fxy },
end

-- 3ª demostración
-- ===============

example
  (h : surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
begin
  intros y yu,
  cases h y with x fxy,
  by finish,
end

import data.set.basic

open set function

variables {α : Type*} {β : Type*}

variable f : α → β

variable u : set β

-- 1ª demostración

-- ===============

example

(h : surjective f)

: u ⊆ f '' (f⁻¹' u) :=

begin

intros y yu,

cases h y with x fxy,

use x,

split,

{ apply mem_preimage.mpr,

rw fxy,

exact yu },

{ exact fxy },

end

-- 2ª demostración

-- ===============

example

(h : surjective f)

: u ⊆ f '' (f⁻¹' u) :=

begin

intros y yu,

cases h y with x fxy,

use x,

split,

{ show f x ∈ u,

rw fxy,

exact yu },

{ exact fxy },

end

-- 3ª demostración

-- ===============

example

(h : surjective f)

: u ⊆ f '' (f⁻¹' u) :=

begin

intros y yu,

cases h y with x fxy,

by finish,

end

Se puede interactuar con la prueba anterior en esta sesión con Lean,
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Imagen_de_imagen_inversa_de_aplicaciones_suprayectivas
imports Main
begin

section ‹1ª demostración›

lemma
  assumes "surj f"
  shows "u ⊆ f ` (f -` u)"
proof (rule subsetI)
  fix y
  assume "y ∈ u"
  have "∃x. y = f x"
    using ‹surj f› by (rule surjD)
  then obtain x where "y = f x"
    by (rule exE)
  then have "f x ∈ u"
    using ‹y ∈ u› by (rule subst)
  then have "x ∈ f -` u"
    by (simp only: vimage_eq)
  then have "f x ∈ f ` (f -` u)"
    by (rule imageI)
  with ‹y = f x› show "y ∈ f ` (f -` u)"
    by (rule ssubst)
qed

section ‹2ª demostración›

lemma
  assumes "surj f"
  shows "u ⊆ f ` (f -` u)"
proof
  fix y
  assume "y ∈ u"
  have "∃x. y = f x"
    using ‹surj f› by (rule surjD)
  then obtain x where "y = f x"
    by (rule exE)
  then have "f x ∈ u"
    using ‹y ∈ u› by simp
  then have "x ∈ f -` u"
    by simp
  then have "f x ∈ f ` (f -` u)"
    by simp
  with ‹y = f x› show "y ∈ f ` (f -` u)"
    by simp
qed

section ‹3ª demostración›

lemma
  assumes "surj f"
  shows "u ⊆ f ` (f -` u)"
  using assms
  by (simp only: surj_image_vimage_eq)

section ‹4ª demostración›

lemma
  assumes "surj f"
  shows "u ⊆ f ` (f -` u)"
  using assms
  unfolding surj_def
  by auto

section ‹5ª demostración›

lemma
  assumes "surj f"
  shows "u ⊆ f ` (f -` u)"
  using assms
  by auto

end

theory Imagen_de_imagen_inversa_de_aplicaciones_suprayectivas

imports Main

begin

section ‹1ª demostración›

lemma

assumes "surj f"

shows "u ⊆ f ` (f -` u)"

proof (rule subsetI)

fix y

assume "y ∈ u"

have "∃x. y = f x"

using ‹surj f› by (rule surjD)

then obtain x where "y = f x"

by (rule exE)

then have "f x ∈ u"

using ‹y ∈ u› by (rule subst)

then have "x ∈ f -` u"

by (simp only: vimage_eq)

then have "f x ∈ f ` (f -` u)"

by (rule imageI)

with ‹y = f x› show "y ∈ f ` (f -` u)"

by (rule ssubst)

qed

section ‹2ª demostración›

lemma

assumes "surj f"

shows "u ⊆ f ` (f -` u)"

proof

fix y

assume "y ∈ u"

have "∃x. y = f x"

using ‹surj f› by (rule surjD)

then obtain x where "y = f x"

by (rule exE)

then have "f x ∈ u"

using ‹y ∈ u› by simp

then have "x ∈ f -` u"

by simp

then have "f x ∈ f ` (f -` u)"

by simp

with ‹y = f x› show "y ∈ f ` (f -` u)"

by simp

qed

section ‹3ª demostración›

lemma

assumes "surj f"

shows "u ⊆ f ` (f -` u)"

using assms

by (simp only: surj_image_vimage_eq)

section ‹4ª demostración›

lemma

assumes "surj f"

shows "u ⊆ f ` (f -` u)"

using assms

unfolding surj_def

by auto

section ‹5ª demostración›

lemma

assumes "surj f"

shows "u ⊆ f ` (f -` u)"

using assms

by auto

end

[/expand]

[expand title=»Nuevas soluciones»]

En los comentarios se pueden escribir nuevas soluciones.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

[/expand]

Imagen de la imagen inversa

PorJosé A. Alonso 10 junio 202112 junio 2021

Demostrar que

   f[f¹[u]] ⊆ u

1	f[f¹[u]] ⊆ u

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  u : set β

example : f '' (f⁻¹' u) ⊆ u :=
sorry

import data.set.basic

open set

variables {α : Type*} {β : Type*}

variable f : α → β

variable u : set β

example : f '' (f⁻¹' u) ⊆ u :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
open set

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  u : set β

-- 1ª demostración
-- ===============

example : f '' (f⁻¹' u) ⊆ u :=
begin
  intros y h,
  cases h with x h2,
  cases h2 with hx fxy,
  rw ← fxy,
  exact hx,
end

-- 2ª demostración
-- ===============

example : f '' (f⁻¹' u) ⊆ u :=
begin
  intros y h,
  rcases h with ⟨x, hx, fxy⟩,
  rw ← fxy,
  exact hx,
end

-- 3ª demostración
-- ===============

example : f '' (f⁻¹' u) ⊆ u :=
begin
  rintros y ⟨x, hx, fxy⟩,
  rw ← fxy,
  exact hx,
end

-- 4ª demostración
-- ===============

example : f '' (f⁻¹' u) ⊆ u :=
begin
  rintros y ⟨x, hx, rfl⟩,
  exact hx,
end

-- 5ª demostración
-- ===============

example : f '' (f⁻¹' u) ⊆ u :=
image_preimage_subset f u

-- 6ª demostración
-- ===============

example : f '' (f⁻¹' u) ⊆ u :=
by simp

import data.set.basic

open set

variables {α : Type*} {β : Type*}

variable f : α → β

variable u : set β

-- 1ª demostración

-- ===============

example : f '' (f⁻¹' u) ⊆ u :=

begin

intros y h,

cases h with x h2,

cases h2 with hx fxy,

rw ← fxy,

exact hx,

end

-- 2ª demostración

-- ===============

example : f '' (f⁻¹' u) ⊆ u :=

begin

intros y h,

rcases h with ⟨x, hx, fxy⟩,

rw ← fxy,

exact hx,

end

-- 3ª demostración

-- ===============

example : f '' (f⁻¹' u) ⊆ u :=

begin

rintros y ⟨x, hx, fxy⟩,

rw ← fxy,

exact hx,

end

-- 4ª demostración

-- ===============

example : f '' (f⁻¹' u) ⊆ u :=

begin

rintros y ⟨x, hx, rfl⟩,

exact hx,

end

-- 5ª demostración

-- ===============

example : f '' (f⁻¹' u) ⊆ u :=

image_preimage_subset f u

-- 6ª demostración

-- ===============

example : f '' (f⁻¹' u) ⊆ u :=

by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean,
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Imagen_de_la_imagen_inversa
imports Main
begin

section ‹1ª demostración›

lemma "f ` (f -` u) ⊆ u"
proof (rule subsetI)
  fix y
  assume "y ∈ f ` (f -` u)"
  then show "y ∈ u"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume "x ∈ f -` u"
    then have "f x ∈ u"
      by (rule vimageD)
    with ‹y = f x› show "y ∈ u"
      by (rule ssubst)
  qed
qed

section ‹2ª demostración›

lemma "f ` (f -` u) ⊆ u"
proof
  fix y
  assume "y ∈ f ` (f -` u)"
  then show "y ∈ u"
  proof
    fix x
    assume "y = f x"
    assume "x ∈ f -` u"
    then have "f x ∈ u"
      by simp
    with ‹y = f x› show "y ∈ u"
      by simp
  qed
qed

section ‹3ª demostración›

lemma "f ` (f -` u) ⊆ u"
  by (simp only: image_vimage_subset)

section ‹4ª demostración›

lemma "f ` (f -` u) ⊆ u"
  by auto

end

theory Imagen_de_la_imagen_inversa

imports Main

begin

section ‹1ª demostración›

lemma "f ` (f -` u) ⊆ u"

proof (rule subsetI)

fix y

assume "y ∈ f ` (f -` u)"

then show "y ∈ u"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ f -` u"

then have "f x ∈ u"

by (rule vimageD)

with ‹y = f x› show "y ∈ u"

by (rule ssubst)

qed

section ‹2ª demostración›

lemma "f ` (f -` u) ⊆ u"

proof

fix y

assume "y ∈ f ` (f -` u)"

then show "y ∈ u"

proof

fix x

assume "y = f x"

assume "x ∈ f -` u"

then have "f x ∈ u"

by simp

with ‹y = f x› show "y ∈ u"

by simp

qed

section ‹3ª demostración›

lemma "f ` (f -` u) ⊆ u"

by (simp only: image_vimage_subset)

section ‹4ª demostración›

lemma "f ` (f -` u) ⊆ u"

by auto

end

[/expand]

[expand title=»Nuevas soluciones»]

En los comentarios se pueden escribir nuevas soluciones.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

[/expand]

Imagen inversa de la imagen de aplicaciones inyectivas

PorJosé A. Alonso 9 junio 202112 junio 2021

Demostrar que si f es inyectiva, entonces

    f⁻¹[f[s]] ⊆ s

1	f⁻¹[f[s]] ⊆ s

Para ello, completar la siguiente teoría de Lean:

import data.set.basic

open set function

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  s : set α

example
  (h : injective f)
  : f ⁻¹' (f '' s) ⊆ s :=
sorry

import data.set.basic

open set function

variables {α : Type*} {β : Type*}

variable f : α → β

variable s : set α

example

(h : injective f)

: f ⁻¹' (f '' s) ⊆ s :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic

open set function

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  s : set α

-- 1ª demostración
-- ===============

example
  (h : injective f)
  : f ⁻¹' (f '' s) ⊆ s :=
begin
  intros x hx,
  rw mem_preimage at hx,
  rw mem_image_eq at hx,
  cases hx with y hy,
  cases hy with ys fyx,
  unfold injective at h,
  have h1 : y = x := h fyx,
  rw ← h1,
  exact ys,
end

-- 2ª demostración
-- ===============

example
  (h : injective f)
  : f ⁻¹' (f '' s) ⊆ s :=
begin
  intros x hx,
  rw mem_preimage at hx,
  rcases hx with ⟨y, ys, fyx⟩,
  rw ← h fyx,
  exact ys,
end

-- 3ª demostración
-- ===============

example
  (h : injective f)
  : f ⁻¹' (f '' s) ⊆ s :=
begin
  rintros x ⟨y, ys, hy⟩,
  rw ← h hy,
  exact ys,
end

import data.set.basic

open set function

variables {α : Type*} {β : Type*}

variable f : α → β

variable s : set α

-- 1ª demostración

-- ===============

example

(h : injective f)

: f ⁻¹' (f '' s) ⊆ s :=

begin

intros x hx,

rw mem_preimage at hx,

rw mem_image_eq at hx,

cases hx with y hy,

cases hy with ys fyx,

unfold injective at h,

have h1 : y = x := h fyx,

rw ← h1,

exact ys,

end

-- 2ª demostración

-- ===============

example

(h : injective f)

: f ⁻¹' (f '' s) ⊆ s :=

begin

intros x hx,

rw mem_preimage at hx,

rcases hx with ⟨y, ys, fyx⟩,

rw ← h fyx,

exact ys,

end

-- 3ª demostración

-- ===============

example

(h : injective f)

: f ⁻¹' (f '' s) ⊆ s :=

begin

rintros x ⟨y, ys, hy⟩,

rw ← h hy,

exact ys,

end

Se puede interactuar con la prueba anterior en esta sesión con Lean,
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Imagen_inversa_de_la_imagen_de_aplicaciones_inyectivas
imports Main
begin

section ‹?ª demostración›

lemma
  assumes "inj f"
  shows "f -` (f ` s) ⊆ s"
proof (rule subsetI)
  fix x
  assume "x ∈ f -` (f ` s)"
  then have "f x ∈ f ` s"
    by (rule vimageD)
  then show "x ∈ s"
  proof (rule imageE)
    fix y
    assume "f x = f y"
    assume "y ∈ s"
    have "x = y"
      using ‹inj f› ‹f x = f y› by (rule injD)
    then show "x ∈ s"
      using ‹y ∈ s›  by (rule ssubst)
  qed
qed

section ‹2ª demostración›

lemma
  assumes "inj f"
  shows "f -` (f ` s) ⊆ s"
proof
  fix x
  assume "x ∈ f -` (f ` s)"
  then have "f x ∈ f ` s"
    by simp
  then show "x ∈ s"
  proof
    fix y
    assume "f x = f y"
    assume "y ∈ s"
    have "x = y"
      using ‹inj f› ‹f x = f y› by (rule injD)
    then show "x ∈ s"
      using ‹y ∈ s›  by simp
  qed
qed

section ‹3ª demostración›

lemma
  assumes "inj f"
  shows "f -` (f ` s) ⊆ s"
  using assms
  unfolding inj_def
  by auto

section ‹4ª demostración›

lemma
  assumes "inj f"
  shows "f -` (f ` s) ⊆ s"
  using assms
  by (simp only: inj_vimage_image_eq)

end

theory Imagen_inversa_de_la_imagen_de_aplicaciones_inyectivas

imports Main

begin

section ‹?ª demostración›

lemma

assumes "inj f"

shows "f -` (f ` s) ⊆ s"

proof (rule subsetI)

fix x

assume "x ∈ f -` (f ` s)"

then have "f x ∈ f ` s"

by (rule vimageD)

then show "x ∈ s"

proof (rule imageE)

fix y

assume "f x = f y"

assume "y ∈ s"

have "x = y"

using ‹inj f› ‹f x = f y› by (rule injD)

then show "x ∈ s"

using ‹y ∈ s› by (rule ssubst)

qed

section ‹2ª demostración›

lemma

assumes "inj f"

shows "f -` (f ` s) ⊆ s"

proof

fix x

assume "x ∈ f -` (f ` s)"

then have "f x ∈ f ` s"

by simp

then show "x ∈ s"

proof

fix y

assume "f x = f y"

assume "y ∈ s"

have "x = y"

using ‹inj f› ‹f x = f y› by (rule injD)

then show "x ∈ s"

using ‹y ∈ s› by simp

qed

section ‹3ª demostración›

lemma

assumes "inj f"

shows "f -` (f ` s) ⊆ s"

using assms

unfolding inj_def

by auto

section ‹4ª demostración›

lemma

assumes "inj f"

shows "f -` (f ` s) ⊆ s"

using assms

by (simp only: inj_vimage_image_eq)

end

[/expand]

[expand title=»Nuevas soluciones»]

En los comentarios se pueden escribir nuevas soluciones.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

[/expand]

Subconjunto de la imagen inversa

PorJosé A. Alonso 8 junio 202112 junio 2021

Demostrar que

   f[s] ⊆ u ↔ s ⊆ f⁻¹[u]

1	f[s] ⊆ u ↔ s ⊆ f⁻¹[u]

Para ello, completar la siguiente teoría de Lean:

import data.set.basic

open set

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  s : set α
variable  u : set β

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=
sorry

import data.set.basic

open set

variables {α : Type*} {β : Type*}

variable f : α → β

variable s : set α

variable u : set β

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic

open set

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  s : set α
variable  u : set β

-- 1ª demostración
-- ===============

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=
begin
  split,
  { intros h x xs,
    apply mem_preimage.mpr,
    apply h,
    apply mem_image_of_mem,
    exact xs, },
  { intros h y hy,
    rcases hy with ⟨x, xs, fxy⟩,
    rw ← fxy,
    exact h xs, },
end

-- 2ª demostración
-- ===============

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=
begin
  split,
  { intros h x xs,
    apply h,
    apply mem_image_of_mem,
    exact xs, },
  { rintros h y ⟨x, xs, rfl⟩,
    exact h xs, },
end

-- 3ª demostración
-- ===============

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=
image_subset_iff

-- 4ª demostración
-- ===============

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=
by simp

import data.set.basic

open set

variables {α : Type*} {β : Type*}

variable f : α → β

variable s : set α

variable u : set β

-- 1ª demostración

-- ===============

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=

begin

split,

{ intros h x xs,

apply mem_preimage.mpr,

apply h,

apply mem_image_of_mem,

exact xs, },

{ intros h y hy,

rcases hy with ⟨x, xs, fxy⟩,

rw ← fxy,

exact h xs, },

end

-- 2ª demostración

-- ===============

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=

begin

split,

{ intros h x xs,

apply h,

apply mem_image_of_mem,

exact xs, },

{ rintros h y ⟨x, xs, rfl⟩,

exact h xs, },

end

-- 3ª demostración

-- ===============

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=

image_subset_iff

-- 4ª demostración

-- ===============

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=

by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean,
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Subconjunto_de_la_imagen_inversa
imports Main
begin

section ‹1ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"
proof (rule iffI)
  assume "f ` s ⊆ u"
  show "s ⊆ f -` u"
  proof (rule subsetI)
    fix x
    assume "x ∈ s"
    then have "f x ∈ f ` s"
      by (simp only: imageI)
    then have "f x ∈ u"
      using ‹f ` s ⊆ u› by (rule set_rev_mp)
    then show "x ∈ f -` u"
      by (simp only: vimageI)
  qed
next
  assume "s ⊆ f -` u"
  show "f ` s ⊆ u"
  proof (rule subsetI)
    fix y
    assume "y ∈ f ` s"
    then show "y ∈ u"
    proof
      fix x
      assume "y = f x"
      assume "x ∈ s"
      then have "x ∈ f -` u"
        using ‹s ⊆ f -` u› by (rule set_rev_mp)
      then have "f x ∈ u"
        by (rule vimageD)
      with ‹y = f x› show "y ∈ u"
        by (rule ssubst)
    qed
  qed
qed

section ‹2ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"
proof
  assume "f ` s ⊆ u"
  show "s ⊆ f -` u"
  proof
    fix x
    assume "x ∈ s"
    then have "f x ∈ f ` s"
      by simp
    then have "f x ∈ u"
      using ‹f ` s ⊆ u› by (simp add: set_rev_mp)
    then show "x ∈ f -` u"
      by simp
  qed
next
  assume "s ⊆ f -` u"
  show "f ` s ⊆ u"
  proof
    fix y
    assume "y ∈ f ` s"
    then show "y ∈ u"
    proof
      fix x
      assume "y = f x"
      assume "x ∈ s"
      then have "x ∈ f -` u"
        using ‹s ⊆ f -` u› by (simp only: set_rev_mp)
      then have "f x ∈ u"
        by simp
      with ‹y = f x› show "y ∈ u"
        by simp
    qed
  qed
qed

section ‹3ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"
  by (simp only: image_subset_iff_subset_vimage)

section ‹4ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"
  by auto

end

theory Subconjunto_de_la_imagen_inversa

imports Main

begin

section ‹1ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"

proof (rule iffI)

assume "f ` s ⊆ u"

show "s ⊆ f -` u"

proof (rule subsetI)

fix x

assume "x ∈ s"

then have "f x ∈ f ` s"

by (simp only: imageI)

then have "f x ∈ u"

using ‹f ` s ⊆ u› by (rule set_rev_mp)

then show "x ∈ f -` u"

by (simp only: vimageI)

qed

assume "s ⊆ f -` u"

show "f ` s ⊆ u"

proof (rule subsetI)

fix y

assume "y ∈ f ` s"

then show "y ∈ u"

proof

fix x

assume "y = f x"

assume "x ∈ s"

then have "x ∈ f -` u"

using ‹s ⊆ f -` u› by (rule set_rev_mp)

then have "f x ∈ u"

by (rule vimageD)

with ‹y = f x› show "y ∈ u"

by (rule ssubst)

qed

section ‹2ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"

proof

assume "f ` s ⊆ u"

show "s ⊆ f -` u"

proof

fix x

assume "x ∈ s"

then have "f x ∈ f ` s"

by simp

then have "f x ∈ u"

using ‹f ` s ⊆ u› by (simp add: set_rev_mp)

then show "x ∈ f -` u"

by simp

qed

assume "s ⊆ f -` u"

show "f ` s ⊆ u"

proof

fix y

assume "y ∈ f ` s"

then show "y ∈ u"

proof

fix x

assume "y = f x"

assume "x ∈ s"

then have "x ∈ f -` u"

using ‹s ⊆ f -` u› by (simp only: set_rev_mp)

then have "f x ∈ u"

by simp

with ‹y = f x› show "y ∈ u"

by simp

qed

section ‹3ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"

by (simp only: image_subset_iff_subset_vimage)

section ‹4ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"

by auto

end

[/expand]

[expand title=»Nuevas soluciones»]

En los comentarios se pueden escribir nuevas soluciones.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

[/expand]

Unión con intersección general

PorJosé A. Alonso 4 junio 20214 junio 2021

Demostrar que

   s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)

1	s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
import tactic

open set

variable  {α : Type}
variable  s : set α
variables A : ℕ → set α

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
sorry

import data.set.basic

import tactic

open set

variable {α : Type}

variable s : set α

variables A : ℕ → set α

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=

sorry

Soluciones

Intersección de intersecciones

PorJosé A. Alonso 3 junio 202121 agosto 2021

Demostrar que

(⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)

1	(⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
import tactic

open set

variable  {α : Type}
variables A B : ℕ → set α

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
sorry

import data.set.basic

import tactic

open set

variable {α : Type}

variables A B : ℕ → set α

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

sorry

Soluciones

Intersección de los primos y los mayores que dos

PorJosé A. Alonso 1 junio 20211 junio 2021

Los conjuntos de los números primos, los mayores que 2 y los impares se definen por

   def primos      : set ℕ := {n | prime n}
   def mayoresQue2 : set ℕ := {n | n > 2}
   def impares     : set ℕ := {n | ¬ even n}

def primos : set ℕ := {n | prime n}

def mayoresQue2 : set ℕ := {n | n > 2}

def impares : set ℕ := {n | ¬ even n}

Demostrar que

   primos ∩ mayoresQue2 ⊆ impares

1	primos ∩ mayoresQue2 ⊆ impares

Para ello, completar la siguiente teoría de Lean:

import data.nat.parity
import data.nat.prime
import tactic

open nat

def primos      : set ℕ := {n | prime n}
def mayoresQue2 : set ℕ := {n | n > 2}
def impares     : set ℕ := {n | ¬ even n}

example : primos ∩ mayoresQue2 ⊆ impares :=
sorry

import data.nat.parity

import data.nat.prime

import tactic

open nat

def primos : set ℕ := {n | prime n}

def mayoresQue2 : set ℕ := {n | n > 2}

def impares : set ℕ := {n | ¬ even n}

example : primos ∩ mayoresQue2 ⊆ impares :=

sorry

Soluciones

Unión de los conjuntos de los pares e impares

PorJosé A. Alonso 31 mayo 202121 agosto 2021

Los conjuntos de los números naturales, de los pares y de los impares se definen por

   def naturales : set ℕ := {n | true}
   def pares     : set ℕ := {n | even n}
   def impares   : set ℕ := {n | ¬ even n}

def naturales : set ℕ := {n | true}

def pares : set ℕ := {n | even n}

def impares : set ℕ := {n | ¬ even n}

Demostrar que

   pares ∪ impares = naturales

1	pares ∪ impares = naturales

Para ello, completar la siguiente teoría de Lean:

import data.nat.parity
import data.set.basic
import tactic

open set

def naturales : set ℕ := {n | true}
def pares     : set ℕ := {n | even n}
def impares   : set ℕ := {n | ¬ even n}

example : pares ∪ impares = naturales :=
sorry

import data.nat.parity

import data.set.basic

import tactic

open set

def naturales : set ℕ := {n | true}

def pares : set ℕ := {n | even n}

def impares : set ℕ := {n | ¬ even n}

example : pares ∪ impares = naturales :=

sorry

Diferencia de unión e intersección

PorJosé A. Alonso 28 mayo 202127 mayo 2021

Demostrar que

(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variable {α : Type}
variables s t : set α

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t : set α

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=

sorry

Soluciones

Unión con su diferencia

PorJosé A. Alonso 27 mayo 202126 mayo 2021

Demostrar que

(s \ t) ∪ t = s ∪ t

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variable {α : Type}
variables s t : set α

example : (s \ t) ∪ t = s ∪ t :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t : set α

example : (s \ t) ∪ t = s ∪ t :=

sorry