Intersección con la imagen inversa

Demostrar que

   s ∩ f⁻¹[v] ⊆ f⁻¹[f[s] ∩ v]

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

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

import data.set.basic

open set

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

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

import data.set.basic

open set

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

variable f : α → β

variable s : set α

variable v : set β

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic

open set

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

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=
begin
  intros x hx,
  rw mem_preimage,
  split,
  { apply mem_image_of_mem,
    exact hx.1, },
  { rw ← mem_preimage,
    exact hx.2, },
end

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=
begin
  rintros x ⟨xs, xv⟩,
  split,
  { exact mem_image_of_mem f xs, },
  { exact xv, },
end

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=
begin
  rintros x ⟨xs, xv⟩,
  exact ⟨mem_image_of_mem f xs, xv⟩,
end

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=
begin
  rintros x ⟨xs, xv⟩,
  show f x ∈ f '' s ∩ v,
  split,
  { use [x, xs, rfl] },
  { exact xv },
end

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=
inter_preimage_subset s v f

import data.set.basic

open set

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

variable f : α → β

variable s : set α

variable v : set β

-- 1ª demostración

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=

begin

intros x hx,

rw mem_preimage,

split,

{ apply mem_image_of_mem,

exact hx.1, },

{ rw ← mem_preimage,

exact hx.2, },

end

-- 2ª demostración

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=

begin

rintros x ⟨xs, xv⟩,

split,

{ exact mem_image_of_mem f xs, },

{ exact xv, },

end

-- 3ª demostración

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=

begin

rintros x ⟨xs, xv⟩,

exact ⟨mem_image_of_mem f xs, xv⟩,

end

-- 4ª demostración

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=

begin

rintros x ⟨xs, xv⟩,

show f x ∈ f '' s ∩ v,

split,

{ use [x, xs, rfl] },

{ exact xv },

end

-- 5ª demostración

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=

inter_preimage_subset s v f

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

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

theory Interseccion_con_la_imagen_inversa
imports Main
begin

(* 1ª demostración *)

lemma "s ∩ f -`  v ⊆ f -` (f ` s ∩ v)"
proof (rule subsetI)
  fix x
  assume "x ∈ s ∩ f -`  v"
  have "f x ∈ f ` s"
  proof -
    have "x ∈ s"
      using ‹x ∈ s ∩ f -`  v› by (rule IntD1)
    then show "f x ∈ f ` s"
      by (rule imageI)
  qed
  moreover
  have "f x ∈ v"
  proof -
    have "x ∈ f -`  v"
      using ‹x ∈ s ∩ f -`  v› by (rule IntD2)
    then show "f x ∈ v"
      by (rule vimageD)
  qed
  ultimately have "f x ∈ f ` s ∩ v"
    by (rule IntI)
  then show "x ∈ f -` (f ` s ∩ v)"
    by (rule vimageI2)
qed

(* 2ª demostración *)

lemma "s ∩ f -`  v ⊆ f -` (f ` s ∩ v)"
proof (rule subsetI)
  fix x
  assume "x ∈ s ∩ f -`  v"
  have "f x ∈ f ` s"
  proof -
    have "x ∈ s" using ‹x ∈ s ∩ f -`  v› by simp
    then show "f x ∈ f ` s" by simp
  qed
  moreover
  have "f x ∈ v"
  proof -
    have "x ∈ f -`  v" using ‹x ∈ s ∩ f -`  v› by simp
    then show "f x ∈ v" by simp
  qed
  ultimately have "f x ∈ f ` s ∩ v" by simp
  then show "x ∈ f -` (f ` s ∩ v)" by simp
qed

(* 3ª demostración *)

lemma "s ∩ f -`  v ⊆ f -` (f ` s ∩ v)"
  by auto

end

theory Interseccion_con_la_imagen_inversa

imports Main

begin

(* 1ª demostración *)

lemma "s ∩ f -` v ⊆ f -` (f ` s ∩ v)"

proof (rule subsetI)

fix x

assume "x ∈ s ∩ f -` v"

have "f x ∈ f ` s"

proof -

have "x ∈ s"

using ‹x ∈ s ∩ f -` v› by (rule IntD1)

then show "f x ∈ f ` s"

by (rule imageI)

qed

moreover

have "f x ∈ v"

proof -

have "x ∈ f -` v"

using ‹x ∈ s ∩ f -` v› by (rule IntD2)

then show "f x ∈ v"

by (rule vimageD)

qed

ultimately have "f x ∈ f ` s ∩ v"

by (rule IntI)

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

by (rule vimageI2)

qed

(* 2ª demostración *)

lemma "s ∩ f -` v ⊆ f -` (f ` s ∩ v)"

proof (rule subsetI)

fix x

assume "x ∈ s ∩ f -` v"

have "f x ∈ f ` s"

proof -

have "x ∈ s" using ‹x ∈ s ∩ f -` v› by simp

then show "f x ∈ f ` s" by simp

qed

moreover

have "f x ∈ v"

proof -

have "x ∈ f -` v" using ‹x ∈ s ∩ f -` v› by simp

then show "f x ∈ v" by simp

qed

ultimately have "f x ∈ f ` s ∩ v" by simp

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

qed

(* 3ª demostración *)

lemma "s ∩ f -` v ⊆ f -` (f ` s ∩ v)"

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Share this:

Escribe un comentarioCancel reply