Imagen inversa de la intersección general

Demostrar que

   f⁻¹[⋂ i, B(i)] = ⋂ i, f⁻¹[B(i)]

1	f⁻¹[⋂ i, B(i)] = ⋂ i, f⁻¹[B(i)]

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

import data.set.basic
import tactic

open set

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
sorry

import data.set.basic

import tactic

open set

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

variable f : α → β

variables B : I → set β

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

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

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
begin
  ext x,
  split,
  { intro hx,
    apply mem_Inter_of_mem,
    intro i,
    rw mem_preimage,
    rw mem_preimage at hx,
    rw mem_Inter at hx,
    exact hx i, },
  { intro hx,
    rw mem_preimage,
    rw mem_Inter,
    intro i,
    rw ← mem_preimage,
    rw mem_Inter at hx,
    exact hx i, },
end

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
begin
  ext x,
  calc  (x ∈ f ⁻¹' ⋂ (i : I), B i)
      ↔ f x ∈ ⋂ (i : I), B i       : mem_preimage
  ... ↔ (∀ i : I, f x ∈ B i)       : mem_Inter
  ... ↔ (∀ i : I, x ∈ f ⁻¹' B i)   : iff_of_eq rfl
  ... ↔ x ∈ ⋂ (i : I), f ⁻¹' B i   : mem_Inter.symm,
end

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
begin
  ext x,
  simp,
end

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
by { ext, simp }

import data.set.basic

import tactic

open set

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

variable f : α → β

variables B : I → set β

-- 1ª demostración

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

begin

ext x,

split,

{ intro hx,

apply mem_Inter_of_mem,

intro i,

rw mem_preimage,

rw mem_preimage at hx,

rw mem_Inter at hx,

exact hx i, },

{ intro hx,

rw mem_preimage,

rw mem_Inter,

intro i,

rw ← mem_preimage,

rw mem_Inter at hx,

exact hx i, },

end

-- 2ª demostración

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

begin

ext x,

calc (x ∈ f ⁻¹' ⋂ (i : I), B i)

↔ f x ∈ ⋂ (i : I), B i : mem_preimage

... ↔ (∀ i : I, f x ∈ B i) : mem_Inter

... ↔ (∀ i : I, x ∈ f ⁻¹' B i) : iff_of_eq rfl

... ↔ x ∈ ⋂ (i : I), f ⁻¹' B i : mem_Inter.symm,

end

-- 3ª demostración

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

begin

ext x,

simp,

end

-- 4ª demostración

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

by { ext, simp }

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 Imagen_inversa_de_la_interseccion_general
imports Main
begin

(* 1ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
proof (rule equalityI)
  show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ f -` (⋂ i ∈ I. B i)"
    show "x ∈ (⋂ i ∈ I. f -` B i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      have "f x ∈ (⋂ i ∈ I. B i)"
        using ‹x ∈ f -` (⋂ i ∈ I. B i)› by (rule vimageD)
      then have "f x ∈ B i"
        using ‹i ∈ I› by (rule INT_D)
      then show "x ∈ f -` B i"
        by (rule vimageI2)
    qed
  qed
next
  show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ (⋂ i ∈ I. f -` B i)"
    have "f x ∈ (⋂ i ∈ I. B i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i"
        by (rule INT_D)
      then show "f x ∈ B i"
        by (rule vimageD)
    qed
    then show "x ∈ f -` (⋂ i ∈ I. B i)"
      by (rule vimageI2)
  qed
qed

(* 2ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
proof
  show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)"
  proof (rule subsetI)
    fix x
    assume hx : "x ∈ f -` (⋂ i ∈ I. B i)"
    show "x ∈ (⋂ i ∈ I. f -` B i)"
    proof
      fix i
      assume "i ∈ I"
      have "f x ∈ (⋂ i ∈ I. B i)" using hx by simp
      then have "f x ∈ B i" using ‹i ∈ I› by simp
      then show "x ∈ f -` B i" by simp
    qed
  qed
next
  show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)"
  proof
    fix x
    assume "x ∈ (⋂ i ∈ I. f -` B i)"
    have "f x ∈ (⋂ i ∈ I. B i)"
    proof
      fix i
      assume "i ∈ I"
      with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i" by simp
      then show "f x ∈ B i" by simp
    qed
    then show "x ∈ f -` (⋂ i ∈ I. B i)" by simp
  qed
qed

(* 3 demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
  by (simp only: vimage_INT)

(* 4ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
  by auto

end

theory Imagen_inversa_de_la_interseccion_general

imports Main

begin

(* 1ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"

proof (rule equalityI)

show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)"

proof (rule subsetI)

fix x

assume "x ∈ f -` (⋂ i ∈ I. B i)"

show "x ∈ (⋂ i ∈ I. f -` B i)"

proof (rule INT_I)

fix i

assume "i ∈ I"

have "f x ∈ (⋂ i ∈ I. B i)"

using ‹x ∈ f -` (⋂ i ∈ I. B i)› by (rule vimageD)

then have "f x ∈ B i"

using ‹i ∈ I› by (rule INT_D)

then show "x ∈ f -` B i"

by (rule vimageI2)

qed

show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)"

proof (rule subsetI)

fix x

assume "x ∈ (⋂ i ∈ I. f -` B i)"

have "f x ∈ (⋂ i ∈ I. B i)"

proof (rule INT_I)

fix i

assume "i ∈ I"

with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i"

by (rule INT_D)

then show "f x ∈ B i"

by (rule vimageD)

qed

then show "x ∈ f -` (⋂ i ∈ I. B i)"

by (rule vimageI2)

qed

(* 2ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"

proof

show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)"

proof (rule subsetI)

fix x

assume hx : "x ∈ f -` (⋂ i ∈ I. B i)"

show "x ∈ (⋂ i ∈ I. f -` B i)"

proof

fix i

assume "i ∈ I"

have "f x ∈ (⋂ i ∈ I. B i)" using hx by simp

then have "f x ∈ B i" using ‹i ∈ I› by simp

then show "x ∈ f -` B i" by simp

qed

show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)"

proof

fix x

assume "x ∈ (⋂ i ∈ I. f -` B i)"

have "f x ∈ (⋂ i ∈ I. B i)"

proof

fix i

assume "i ∈ I"

with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i" by simp

then show "f x ∈ B i" by simp

qed

then show "x ∈ f -` (⋂ i ∈ I. B i)" by simp

qed

(* 3 demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"

by (simp only: vimage_INT)

(* 4ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"

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