junio 2021 – Página 3

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