DAO: La semana en Calculemus (del 25 al 30 de abril)

Esta semana he publicado en Calculemus las soluciones de los siguientes problemas:

1. Intersección con su unión
2. Distributiva de la intersección respecto de la unión general
3. Imagen inversa de la intersección

A continuación se muestran las soluciones.

1. Intersección con su unión

Demostrar que s ∩ (s ∪ t) = s

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

import data.set.basic
open set

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

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

import data.set.basic

open set

variable {α : Type}

variables s t : set α

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

sorry

Soluciones con Lean

import data.set.basic
import tactic
open set

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

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

example : s ∩ (s ∪ t) = s :=
begin
  ext x,
  split,
  { intros h,
    dsimp at h,
    exact h.1, },
  { intro xs,
    dsimp,
    split,
    { exact xs, },
    { left,
      exact xs, }},
end

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

example : s ∩ (s ∪ t) = s :=
begin
  ext x,
  split,
  { intros h,
    exact h.1, },
  { intro xs,
    split,
    { exact xs, },
    { left,
      exact xs, }},
end

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

example : s ∩ (s ∪ t) = s :=
begin
  ext x,
  split,
  { intros h,
    exact h.1, },
  { intro xs,
    split,
    { exact xs, },
    { exact (or.inl xs), }},
end

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

example : s ∩ (s ∪ t) = s :=
begin
  ext,
  exact ⟨λ h, h.1,
         λ xs, ⟨xs, or.inl xs⟩⟩,
end

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

example : s ∩ (s ∪ t) = s :=
begin
  ext,
  exact ⟨and.left,
         λ xs, ⟨xs, or.inl xs⟩⟩,
end

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

example : s ∩ (s ∪ t) = s :=
begin
  ext x,
  split,
  { rintros ⟨xs, _⟩,
    exact xs },
  { intro xs,
    use xs,
    left,
    exact xs },
end

-- 7ª demostración
-- ===============

example : s ∩ (s ∪ t) = s :=
begin
  apply subset_antisymm,
  { rintros x ⟨hxs,-⟩,
    exact hxs, },
  { intros x hxs,
    exact ⟨hxs, or.inl hxs⟩, },
end

-- 8ª demostración
-- ===============

example : s ∩ (s ∪ t) = s :=
-- by suggest
inf_sup_self

-- 9ª demostración
-- ===============

example : s ∩ (s ∪ t) = s :=
-- by hint
by finish

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

import data.set.basic

import tactic

open set

variable {α : Type}

variables s t : set α

-- 1ª demostración

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

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

begin

ext x,

split,

{ intros h,

dsimp at h,

exact h.1, },

{ intro xs,

dsimp,

split,

{ exact xs, },

{ left,

exact xs, }},

end

-- 2ª demostración

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

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

begin

ext x,

split,

{ intros h,

exact h.1, },

{ intro xs,

split,

{ exact xs, },

{ left,

exact xs, }},

end

-- 3ª demostración

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

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

begin

ext x,

split,

{ intros h,

exact h.1, },

{ intro xs,

split,

{ exact xs, },

{ exact (or.inl xs), }},

end

-- 4ª demostración

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

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

begin

ext,

exact ⟨λ h, h.1,

λ xs, ⟨xs, or.inl xs⟩⟩,

end

-- 5ª demostración

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

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

begin

ext,

exact ⟨and.left,

λ xs, ⟨xs, or.inl xs⟩⟩,

end

-- 6ª demostración

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

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

begin

ext x,

split,

{ rintros ⟨xs, _⟩,

exact xs },

{ intro xs,

use xs,

left,

exact xs },

end

-- 7ª demostración

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

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

begin

apply subset_antisymm,

{ rintros x ⟨hxs,-⟩,

exact hxs, },

{ intros x hxs,

exact ⟨hxs, or.inl hxs⟩, },

end

-- 8ª demostración

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

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

-- by suggest

inf_sup_self

-- 9ª demostración

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

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

-- by hint

by finish

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL

theory Interseccion_con_su_union
imports Main
begin

(* 1ª demostración *)
lemma "s ∩ (s ∪ t) = s"
proof (rule  equalityI)
  show "s ∩ (s ∪ t) ⊆ s"
  proof (rule subsetI)
    fix x
    assume "x ∈ s ∩ (s ∪ t)"
    then show "x ∈ s"
      by (simp only: IntD1)
  qed
next
  show "s ⊆ s ∩ (s ∪ t)"
  proof (rule subsetI)
    fix x
    assume "x ∈ s"
    then have "x ∈ s ∪ t"
      by (simp only: UnI1)
    with ‹x ∈ s› show "x ∈ s ∩ (s ∪ t)"
      by (rule IntI)
  qed
qed

(* 2ª demostración *)
lemma "s ∩ (s ∪ t) = s"
proof
  show "s ∩ (s ∪ t) ⊆ s"
  proof
    fix x
    assume "x ∈ s ∩ (s ∪ t)"
    then show "x ∈ s"
      by simp
  qed
next
  show "s ⊆ s ∩ (s ∪ t)"
  proof
    fix x
    assume "x ∈ s"
    then have "x ∈ s ∪ t"
      by simp
    then show "x ∈ s ∩ (s ∪ t)"
      using ‹x ∈ s› by simp
  qed
qed

(* 3ª demostración *)
lemma "s ∩ (s ∪ t) = s"
by (fact Un_Int_eq)

(* 4ª demostración *)
lemma "s ∩ (s ∪ t) = s"
by auto

theory Interseccion_con_su_union

imports Main

begin

(* 1ª demostración *)

lemma "s ∩ (s ∪ t) = s"

proof (rule equalityI)

show "s ∩ (s ∪ t) ⊆ s"

proof (rule subsetI)

fix x

assume "x ∈ s ∩ (s ∪ t)"

then show "x ∈ s"

by (simp only: IntD1)

qed

show "s ⊆ s ∩ (s ∪ t)"

proof (rule subsetI)

fix x

assume "x ∈ s"

then have "x ∈ s ∪ t"

by (simp only: UnI1)

with ‹x ∈ s› show "x ∈ s ∩ (s ∪ t)"

by (rule IntI)

qed

(* 2ª demostración *)

lemma "s ∩ (s ∪ t) = s"

proof

show "s ∩ (s ∪ t) ⊆ s"

proof

fix x

assume "x ∈ s ∩ (s ∪ t)"

then show "x ∈ s"

by simp

qed

show "s ⊆ s ∩ (s ∪ t)"

proof

fix x

assume "x ∈ s"

then have "x ∈ s ∪ t"

by simp

then show "x ∈ s ∩ (s ∪ t)"

using ‹x ∈ s› by simp

qed

(* 3ª demostración *)

lemma "s ∩ (s ∪ t) = s"

by (fact Un_Int_eq)

(* 4ª demostración *)

lemma "s ∩ (s ∪ t) = s"

by auto

2. Distributiva de la intersección respecto de la unión general

Demostrar que s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s)

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

import data.set.basic
import data.set.lattice
import tactic

open set

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
sorry

import data.set.basic

import data.set.lattice

import tactic

open set

variable {α : Type}

variable s : set α

variable A : ℕ → set α

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

sorry

Soluciones con Lean

import data.set.basic
import data.set.lattice
import tactic

open set

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

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
begin
  ext x,
  split,
  { intro h,
    rw mem_Union,
    cases h with xs xUAi,
    rw mem_Union at xUAi,
    cases xUAi with i xAi,
    use i,
    split,
    { exact xAi, },
    { exact xs, }},
  { intro h,
    rw mem_Union at h,
    cases h with i hi,
    cases hi with xAi xs,
    split,
    { exact xs, },
    { rw mem_Union,
      use i,
      exact xAi, }},
end

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
begin
  ext x,
  simp,
  split,
  { rintros ⟨xs, ⟨i, xAi⟩⟩,
    exact ⟨⟨i, xAi⟩, xs⟩, },
  { rintros ⟨⟨i, xAi⟩, xs⟩,
    exact ⟨xs, ⟨i, xAi⟩⟩ },
end

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
begin
  ext x,
  finish,
end

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
by ext; finish

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
by finish [ext_iff]

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
by tidy

import data.set.basic

import data.set.lattice

import tactic

open set

variable {α : Type}

variable s : set α

variable A : ℕ → set α

-- 1ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

begin

ext x,

split,

{ intro h,

rw mem_Union,

cases h with xs xUAi,

rw mem_Union at xUAi,

cases xUAi with i xAi,

use i,

split,

{ exact xAi, },

{ exact xs, }},

{ intro h,

rw mem_Union at h,

cases h with i hi,

cases hi with xAi xs,

split,

{ exact xs, },

{ rw mem_Union,

use i,

exact xAi, }},

end

-- 2ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

begin

ext x,

simp,

split,

{ rintros ⟨xs, ⟨i, xAi⟩⟩,

exact ⟨⟨i, xAi⟩, xs⟩, },

{ rintros ⟨⟨i, xAi⟩, xs⟩,

exact ⟨xs, ⟨i, xAi⟩⟩ },

end

-- 3ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

begin

ext x,

finish,

end

-- 4ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

by ext; finish

-- 5ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

by finish [ext_iff]

-- 6ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

by tidy

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL

theory Distributiva_de_la_interseccion_respecto_de_la_union_general
imports Main
begin

section ‹1ª demostración›

lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))"
proof (rule equalityI)
  show "s ∩ (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. (A i ∩ s))"
  proof (rule subsetI)
    fix x
    assume "x ∈ s ∩ (⋃ i ∈ I. A i)"
    then have "x ∈ s"
      by (simp only: IntD1)
    have "x ∈ (⋃ i ∈ I. A i)"
      using ‹x ∈ s ∩ (⋃ i ∈ I. A i)› by (simp only: IntD2)
    then show "x ∈ (⋃ i ∈ I. (A i ∩ s))"
    proof (rule UN_E)
      fix i
      assume "i ∈ I"
      assume "x ∈ A i"
      then have "x ∈ A i ∩ s"
        using ‹x ∈ s› by (rule IntI)
      with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. (A i ∩ s))"
        by (rule UN_I)
    qed
  qed
next
  show "(⋃ i ∈ I. (A i ∩ s)) ⊆ s ∩ (⋃ i ∈ I. A i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ (⋃ i ∈ I. A i ∩ s)"
    then show "x ∈ s ∩ (⋃ i ∈ I. A i)"
    proof (rule UN_E)
      fix i
      assume "i ∈ I"
      assume "x ∈ A i ∩ s"
      then have "x ∈ A i"
        by (rule IntD1)
      have "x ∈ s"
        using ‹x ∈ A i ∩ s› by (rule IntD2)
      moreover
      have "x ∈ (⋃ i ∈ I. A i)"
        using ‹i ∈ I› ‹x ∈ A i› by (rule UN_I)
      ultimately show "x ∈ s ∩ (⋃ i ∈ I. A i)"
        by (rule IntI)
    qed
  qed
qed

section ‹2ª demostración›

lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))"
proof
  show "s ∩ (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. (A i ∩ s))"
  proof
    fix x
    assume "x ∈ s ∩ (⋃ i ∈ I. A i)"
    then have "x ∈ s"
      by simp
    have "x ∈ (⋃ i ∈ I. A i)"
      using ‹x ∈ s ∩ (⋃ i ∈ I. A i)› by simp
    then show "x ∈ (⋃ i ∈ I. (A i ∩ s))"
    proof
      fix i
      assume "i ∈ I"
      assume "x ∈ A i"
      then have "x ∈ A i ∩ s"
        using ‹x ∈ s› by simp
      with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. (A i ∩ s))"
        by (rule UN_I)
    qed
  qed
next
  show "(⋃ i ∈ I. (A i ∩ s)) ⊆ s ∩ (⋃ i ∈ I. A i)"
  proof
    fix x
    assume "x ∈ (⋃ i ∈ I. A i ∩ s)"
    then show "x ∈ s ∩ (⋃ i ∈ I. A i)"
    proof
      fix i
      assume "i ∈ I"
      assume "x ∈ A i ∩ s"
      then have "x ∈ A i"
        by simp
      have "x ∈ s"
        using ‹x ∈ A i ∩ s› by simp
      moreover
      have "x ∈ (⋃ i ∈ I. A i)"
        using ‹i ∈ I› ‹x ∈ A i› by (rule UN_I)
      ultimately show "x ∈ s ∩ (⋃ i ∈ I. A i)"
        by simp
    qed
  qed
qed

section ‹3ª demostración›

lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))"
  by auto

end

100

101

102

theory Distributiva_de_la_interseccion_respecto_de_la_union_general

imports Main

begin

section ‹1ª demostración›

lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))"

proof (rule equalityI)

show "s ∩ (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. (A i ∩ s))"

proof (rule subsetI)

fix x

assume "x ∈ s ∩ (⋃ i ∈ I. A i)"

then have "x ∈ s"

by (simp only: IntD1)

have "x ∈ (⋃ i ∈ I. A i)"

using ‹x ∈ s ∩ (⋃ i ∈ I. A i)› by (simp only: IntD2)

then show "x ∈ (⋃ i ∈ I. (A i ∩ s))"

proof (rule UN_E)

fix i

assume "i ∈ I"

assume "x ∈ A i"

then have "x ∈ A i ∩ s"

using ‹x ∈ s› by (rule IntI)

with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. (A i ∩ s))"

by (rule UN_I)

qed

show "(⋃ i ∈ I. (A i ∩ s)) ⊆ s ∩ (⋃ i ∈ I. A i)"

proof (rule subsetI)

fix x

assume "x ∈ (⋃ i ∈ I. A i ∩ s)"

then show "x ∈ s ∩ (⋃ i ∈ I. A i)"

proof (rule UN_E)

fix i

assume "i ∈ I"

assume "x ∈ A i ∩ s"

then have "x ∈ A i"

by (rule IntD1)

have "x ∈ s"

using ‹x ∈ A i ∩ s› by (rule IntD2)

moreover

have "x ∈ (⋃ i ∈ I. A i)"

using ‹i ∈ I› ‹x ∈ A i› by (rule UN_I)

ultimately show "x ∈ s ∩ (⋃ i ∈ I. A i)"

by (rule IntI)

qed

section ‹2ª demostración›

lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))"

proof

show "s ∩ (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. (A i ∩ s))"

proof

fix x

assume "x ∈ s ∩ (⋃ i ∈ I. A i)"

then have "x ∈ s"

by simp

have "x ∈ (⋃ i ∈ I. A i)"

using ‹x ∈ s ∩ (⋃ i ∈ I. A i)› by simp

then show "x ∈ (⋃ i ∈ I. (A i ∩ s))"

proof

fix i

assume "i ∈ I"

assume "x ∈ A i"

then have "x ∈ A i ∩ s"

using ‹x ∈ s› by simp

with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. (A i ∩ s))"

by (rule UN_I)

qed

show "(⋃ i ∈ I. (A i ∩ s)) ⊆ s ∩ (⋃ i ∈ I. A i)"

proof

fix x

assume "x ∈ (⋃ i ∈ I. A i ∩ s)"

then show "x ∈ s ∩ (⋃ i ∈ I. A i)"

proof

fix i

assume "i ∈ I"

assume "x ∈ A i ∩ s"

then have "x ∈ A i"

by simp

have "x ∈ s"

using ‹x ∈ A i ∩ s› by simp

moreover

have "x ∈ (⋃ i ∈ I. A i)"

using ‹i ∈ I› ‹x ∈ A i› by (rule UN_I)

ultimately show "x ∈ s ∩ (⋃ i ∈ I. A i)"

by simp

qed

section ‹3ª demostración›

lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))"

by auto

end

3. Imagen inversa de la intersección

En Lean, la imagen inversa de un conjunto s (de elementos de tipo por la función f (de tipo α → β) es el conjunto f ⁻¹' s de elementos x (de tipo α) tales que f x ∈ s.

Demostrar que f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v

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

import data.set.basic

open set

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=
sorry

import data.set.basic

open set

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

variable f : α → β

variables u v : set β

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=

sorry

Soluciones con Lean

import data.set.basic

open set

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

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=
begin
  ext x,
  split,
  { intro h,
    split,
    { apply mem_preimage.mpr,
      rw mem_preimage at h,
      exact mem_of_mem_inter_left h, },
    { apply mem_preimage.mpr,
      rw mem_preimage at h,
      exact mem_of_mem_inter_right h, }},
  { intro h,
    apply mem_preimage.mpr,
    split,
    { apply mem_preimage.mp,
      exact mem_of_mem_inter_left h,},
    { apply mem_preimage.mp,
      exact mem_of_mem_inter_right h, }},
end

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=
begin
  ext x,
  split,
  { intro h,
    split,
    { simp at *,
      exact h.1, },
    { simp at *,
      exact h.2, }},
  { intro h,
    simp at *,
    exact h, },
end

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=
-- by hint
by finish

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=
-- by library_search
preimage_inter

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=
rfl

import data.set.basic

open set

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

variable f : α → β

variables u v : set β

-- 1ª demostración

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=

begin

ext x,

split,

{ intro h,

split,

{ apply mem_preimage.mpr,

rw mem_preimage at h,

exact mem_of_mem_inter_left h, },

{ apply mem_preimage.mpr,

rw mem_preimage at h,

exact mem_of_mem_inter_right h, }},

{ intro h,

apply mem_preimage.mpr,

split,

{ apply mem_preimage.mp,

exact mem_of_mem_inter_left h,},

{ apply mem_preimage.mp,

exact mem_of_mem_inter_right h, }},

end

-- 2ª demostración

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=

begin

ext x,

split,

{ intro h,

split,

{ simp at *,

exact h.1, },

{ simp at *,

exact h.2, }},

{ intro h,

simp at *,

exact h, },

end

-- 3ª demostración

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=

-- by hint

by finish

-- 4ª demostración

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=

-- by library_search

preimage_inter

-- 5ª demostración

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

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=

rfl

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL

theory Imagen_inversa_de_la_interseccion
imports Main
begin

section ‹1ª demostración›

lemma "f -` (u ∩ v) = f -` u ∩ f -` v"
proof (rule equalityI)
  show "f -` (u ∩ v) ⊆ f -` u ∩ f -` v"
  proof (rule subsetI)
    fix x
    assume "x ∈ f -` (u ∩ v)"
    then have h : "f x ∈ u ∩ v"
      by (simp only: vimage_eq)
    have "x ∈ f -` u"
    proof -
      have "f x ∈ u"
        using h by (rule IntD1)
      then show "x ∈ f -` u"
        by (rule vimageI2)
    qed
    moreover
    have "x ∈ f -` v"
    proof -
      have "f x ∈ v"
        using h by (rule IntD2)
      then show "x ∈ f -` v"
        by (rule vimageI2)
    qed
    ultimately show "x ∈ f -` u ∩ f -` v"
      by (rule IntI)
  qed
next
  show "f -` u ∩ f -` v ⊆ f -` (u ∩ v)"
  proof (rule subsetI)
    fix x
    assume h2 : "x ∈ f -` u ∩ f -` v"
    have "f x ∈ u"
    proof -
      have "x ∈ f -` u"
        using h2 by (rule IntD1)
      then show "f x ∈ u"
        by (rule vimageD)
    qed
    moreover
    have "f x ∈ v"
    proof -
      have "x ∈ f -` v"
        using h2 by (rule IntD2)
      then show "f x ∈ v"
        by (rule vimageD)
    qed
    ultimately have "f x ∈ u ∩ v"
      by (rule IntI)
    then show "x ∈ f -` (u ∩ v)"
      by (rule vimageI2)
  qed
qed

section ‹2ª demostración›

lemma "f -` (u ∩ v) = f -` u ∩ f -` v"
proof
  show "f -` (u ∩ v) ⊆ f -` u ∩ f -` v"
  proof
    fix x
    assume "x ∈ f -` (u ∩ v)"
    then have h : "f x ∈ u ∩ v"
      by simp
    have "x ∈ f -` u"
    proof -
      have "f x ∈ u"
        using h by simp
      then show "x ∈ f -` u"
        by simp
    qed
    moreover
    have "x ∈ f -` v"
    proof -
      have "f x ∈ v"
        using h by simp
      then show "x ∈ f -` v"
        by simp
    qed
    ultimately show "x ∈ f -` u ∩ f -` v"
      by simp
  qed
next
  show "f -` u ∩ f -` v ⊆ f -` (u ∩ v)"
  proof
    fix x
    assume h2 : "x ∈ f -` u ∩ f -` v"
    have "f x ∈ u"
    proof -
      have "x ∈ f -` u"
        using h2 by simp
      then show "f x ∈ u"
        by simp
    qed
    moreover
    have "f x ∈ v"
    proof -
      have "x ∈ f -` v"
        using h2 by simp
      then show "f x ∈ v"
        by simp
    qed
    ultimately have "f x ∈ u ∩ v"
      by simp
    then show "x ∈ f -` (u ∩ v)"
      by simp
  qed
qed

section ‹3ª demostración›

lemma "f -` (u ∩ v) = f -` u ∩ f -` v"
proof
  show "f -` (u ∩ v) ⊆ f -` u ∩ f -` v"
  proof
    fix x
    assume h1 : "x ∈ f -` (u ∩ v)"
    have "x ∈ f -` u" using h1 by simp
    moreover
    have "x ∈ f -` v" using h1 by simp
    ultimately show "x ∈ f -` u ∩ f -` v" by simp
  qed
next
  show "f -` u ∩ f -` v ⊆ f -` (u ∩ v)"
  proof
    fix x
    assume h2 : "x ∈ f -` u ∩ f -` v"
    have "f x ∈ u" using h2 by simp
    moreover
    have "f x ∈ v" using h2 by simp
    ultimately have "f x ∈ u ∩ v" by simp
    then show "x ∈ f -` (u ∩ v)" by simp
  qed
qed

section ‹4ª demostración›

lemma "f -` (u ∩ v) = f -` u ∩ f -` v"
  by (simp only: vimage_Int)

section ‹5ª demostración›

lemma "f -` (u ∩ v) = f -` u ∩ f -` v"
  by auto

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

theory Imagen_inversa_de_la_interseccion

imports Main

begin

section ‹1ª demostración›

lemma "f -` (u ∩ v) = f -` u ∩ f -` v"

proof (rule equalityI)

show "f -` (u ∩ v) ⊆ f -` u ∩ f -` v"

proof (rule subsetI)

fix x

assume "x ∈ f -` (u ∩ v)"

then have h : "f x ∈ u ∩ v"

by (simp only: vimage_eq)

have "x ∈ f -` u"

proof -

have "f x ∈ u"

using h by (rule IntD1)

then show "x ∈ f -` u"

by (rule vimageI2)

qed

moreover

have "x ∈ f -` v"

proof -

have "f x ∈ v"

using h by (rule IntD2)

then show "x ∈ f -` v"

by (rule vimageI2)

qed

ultimately show "x ∈ f -` u ∩ f -` v"

by (rule IntI)

qed

show "f -` u ∩ f -` v ⊆ f -` (u ∩ v)"

proof (rule subsetI)

fix x

assume h2 : "x ∈ f -` u ∩ f -` v"

have "f x ∈ u"

proof -

have "x ∈ f -` u"

using h2 by (rule IntD1)

then show "f x ∈ u"

by (rule vimageD)

qed

moreover

have "f x ∈ v"

proof -

have "x ∈ f -` v"

using h2 by (rule IntD2)

then show "f x ∈ v"

by (rule vimageD)

qed

ultimately have "f x ∈ u ∩ v"

by (rule IntI)

then show "x ∈ f -` (u ∩ v)"

by (rule vimageI2)

qed

section ‹2ª demostración›

lemma "f -` (u ∩ v) = f -` u ∩ f -` v"

proof

show "f -` (u ∩ v) ⊆ f -` u ∩ f -` v"

proof

fix x

assume "x ∈ f -` (u ∩ v)"

then have h : "f x ∈ u ∩ v"

by simp

have "x ∈ f -` u"

proof -

have "f x ∈ u"

using h by simp

then show "x ∈ f -` u"

by simp

qed

moreover

have "x ∈ f -` v"

proof -

have "f x ∈ v"

using h by simp

then show "x ∈ f -` v"

by simp

qed

ultimately show "x ∈ f -` u ∩ f -` v"

by simp

qed

show "f -` u ∩ f -` v ⊆ f -` (u ∩ v)"

proof

fix x

assume h2 : "x ∈ f -` u ∩ f -` v"

have "f x ∈ u"

proof -

have "x ∈ f -` u"

using h2 by simp

then show "f x ∈ u"

by simp

qed

moreover

have "f x ∈ v"

proof -

have "x ∈ f -` v"

using h2 by simp

then show "f x ∈ v"

by simp

qed

ultimately have "f x ∈ u ∩ v"

by simp

then show "x ∈ f -` (u ∩ v)"

by simp

qed

section ‹3ª demostración›

lemma "f -` (u ∩ v) = f -` u ∩ f -` v"

proof

show "f -` (u ∩ v) ⊆ f -` u ∩ f -` v"

proof

fix x

assume h1 : "x ∈ f -` (u ∩ v)"

have "x ∈ f -` u" using h1 by simp

moreover

have "x ∈ f -` v" using h1 by simp

ultimately show "x ∈ f -` u ∩ f -` v" by simp

qed

show "f -` u ∩ f -` v ⊆ f -` (u ∩ v)"

proof

fix x

assume h2 : "x ∈ f -` u ∩ f -` v"

have "f x ∈ u" using h2 by simp

moreover

have "f x ∈ v" using h2 by simp

ultimately have "f x ∈ u ∩ v" by simp

then show "x ∈ f -` (u ∩ v)" by simp

qed

section ‹4ª demostración›

lemma "f -` (u ∩ v) = f -` u ∩ f -` v"

by (simp only: vimage_Int)

section ‹5ª demostración›

lemma "f -` (u ∩ v) = f -` u ∩ f -` v"

by auto

end

1. Intersección con su unión

2. Distributiva de la intersección respecto de la unión general

3. Imagen inversa de la intersección

Se puede imprimir o compartir con