24 junio 2021 – Calculemus

Imagen de la intersección general

PorJosé A. Alonso 24 junio 202115 junio 2021

Demostrar que

   f[⋂ i, A i] ⊆ ⋂ i, f[A i]

1	f[⋂ i, A i] ⊆ ⋂ i, f[A 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 A : ℕ → set α

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
sorry

import data.set.basic

import tactic

open set

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

variable f : α → β

variables A : ℕ → set α

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

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

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
begin
  intros y h,
  apply mem_Inter_of_mem,
  intro i,
  cases h with x hx,
  cases hx with xIA fxy,
  rw ← fxy,
  apply mem_image_of_mem,
  exact mem_Inter.mp xIA i,
end

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
begin
  intros y h,
  apply mem_Inter_of_mem,
  intro i,
  rcases h with ⟨x, xIA, rfl⟩,
  exact mem_image_of_mem f (mem_Inter.mp xIA i),
end

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
begin
  intro y,
  simp,
  intros x xIA fxy i,
  use [x, xIA i, fxy],
end

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
by tidy

import data.set.basic

import tactic

open set

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

variable f : α → β

variables A : ℕ → set α

-- 1ª demostración

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

begin

intros y h,

apply mem_Inter_of_mem,

intro i,

cases h with x hx,

cases hx with xIA fxy,

rw ← fxy,

apply mem_image_of_mem,

exact mem_Inter.mp xIA i,

end

-- 2ª demostración

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

begin

intros y h,

apply mem_Inter_of_mem,

intro i,

rcases h with ⟨x, xIA, rfl⟩,

exact mem_image_of_mem f (mem_Inter.mp xIA i),

end

-- 3ª demostración

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

begin

intro y,

simp,

intros x xIA fxy i,

use [x, xIA i, fxy],

end

-- 4ª demostración

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

by tidy

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

(* 1ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"
proof (rule subsetI)
  fix y
  assume "y ∈ f ` (⋂ i ∈ I. A i)"
  then show "y ∈ (⋂ i ∈ I. f ` A i)"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume xIA : "x ∈ (⋂ i ∈ I. A i)"
    have "f x ∈ (⋂ i ∈ I. f ` A i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      with xIA have "x ∈ A i"
        by (rule INT_D)
      then show "f x ∈ f ` A i"
        by (rule imageI)
    qed
    with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)"
      by (rule ssubst)
  qed
qed

(* 2ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"
proof
  fix y
  assume "y ∈ f ` (⋂ i ∈ I. A i)"
  then show "y ∈ (⋂ i ∈ I. f ` A i)"
  proof
    fix x
    assume "y = f x"
    assume xIA : "x ∈ (⋂ i ∈ I. A i)"
    have "f x ∈ (⋂ i ∈ I. f ` A i)"
    proof
      fix i
      assume "i ∈ I"
      with xIA have "x ∈ A i" by simp
      then show "f x ∈ f ` A i" by simp
    qed
    with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)" by simp
  qed
qed

(* 3ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"
  by auto

end

theory Imagen_de_la_interseccion_general

imports Main

begin

(* 1ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"

proof (rule subsetI)

fix y

assume "y ∈ f ` (⋂ i ∈ I. A i)"

then show "y ∈ (⋂ i ∈ I. f ` A i)"

proof (rule imageE)

fix x

assume "y = f x"

assume xIA : "x ∈ (⋂ i ∈ I. A i)"

have "f x ∈ (⋂ i ∈ I. f ` A i)"

proof (rule INT_I)

fix i

assume "i ∈ I"

with xIA have "x ∈ A i"

by (rule INT_D)

then show "f x ∈ f ` A i"

by (rule imageI)

qed

with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)"

by (rule ssubst)

qed

(* 2ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"

proof

fix y

assume "y ∈ f ` (⋂ i ∈ I. A i)"

then show "y ∈ (⋂ i ∈ I. f ` A i)"

proof

fix x

assume "y = f x"

assume xIA : "x ∈ (⋂ i ∈ I. A i)"

have "f x ∈ (⋂ i ∈ I. f ` A i)"

proof

fix i

assume "i ∈ I"

with xIA have "x ∈ A i" by simp

then show "f x ∈ f ` A i" by simp

qed

with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)" by simp

qed

(* 3ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A 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]