12 junio 2021 – Calculemus

Monotonía de la imagen de conjuntos

PorJosé A. Alonso 12 junio 202112 junio 2021

Demostrar que si s ⊆ t, entonces

    f[s] ⊆ f[t]

1	f[s] ⊆ f[t]

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

import data.set.basic
import tactic

open set

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
sorry

import data.set.basic

import tactic

open set

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

variable f : α → β

variables s t : set α

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

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

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
begin
  intros y hy,
  rw mem_image at hy,
  cases hy with x hx,
  cases hx with xs fxy,
  use x,
  split,
  { exact h xs, },
  { exact fxy, },
end

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
begin
  intros y hy,
  rcases hy with ⟨x, xs, fxy⟩,
  use x,
  exact ⟨h xs, fxy⟩,
end

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
begin
  rintros y ⟨x, xs, fxy ⟩,
  use [x, h xs, fxy],
end

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
by finish [subset_def, mem_image_eq]

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
image_subset f h

import data.set.basic

import tactic

open set

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

variable f : α → β

variables s t : set α

-- 1ª demostración

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

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

begin

intros y hy,

rw mem_image at hy,

cases hy with x hx,

cases hx with xs fxy,

use x,

split,

{ exact h xs, },

{ exact fxy, },

end

-- 2ª demostración

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

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

begin

intros y hy,

rcases hy with ⟨x, xs, fxy⟩,

use x,

exact ⟨h xs, fxy⟩,

end

-- 3ª demostración

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

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

begin

rintros y ⟨x, xs, fxy ⟩,

use [x, h xs, fxy],

end

-- 4ª demostración

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

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

by finish [subset_def, mem_image_eq]

-- 5ª demostración

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

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

image_subset f h

Se puede interactuar con la prueba anterior en esta sesión con Lean,
[/expand]

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

theory Monotonia_de_la_imagen_de_conjuntos
imports Main
begin

section ‹1ª demostración›

lemma
  assumes "s ⊆ t"
  shows "f ` s ⊆ f ` t"
proof (rule subsetI)
  fix y
  assume "y ∈ f ` s"
  then show "y ∈ f ` t"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume "x ∈ s"
    then have "x ∈ t"
      using ‹s ⊆ t› by (simp only: set_rev_mp)
    then have "f x ∈ f ` t"
      by (rule imageI)
    with ‹y = f x› show "y ∈ f ` t"
      by (rule ssubst)
  qed
qed

section ‹2ª demostración›

lemma
  assumes "s ⊆ t"
  shows "f ` s ⊆ f ` t"
proof
  fix y
  assume "y ∈ f ` s"
  then show "y ∈ f ` t"
  proof
    fix x
    assume "y = f x"
    assume "x ∈ s"
    then have "x ∈ t"
      using ‹s ⊆ t› by (simp only: set_rev_mp)
    then have "f x ∈ f ` t"
      by simp
    with ‹y = f x› show "y ∈ f ` t"
      by simp
  qed
qed

section ‹3ª demostración›

lemma
  assumes "s ⊆ t"
  shows "f ` s ⊆ f ` t"
  using assms
  by blast

section ‹4ª demostración›

lemma
  assumes "s ⊆ t"
  shows "f ` s ⊆ f ` t"
  using assms
  by (simp only: image_mono)

end

theory Monotonia_de_la_imagen_de_conjuntos

imports Main

begin

section ‹1ª demostración›

lemma

assumes "s ⊆ t"

shows "f ` s ⊆ f ` t"

proof (rule subsetI)

fix y

assume "y ∈ f ` s"

then show "y ∈ f ` t"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ s"

then have "x ∈ t"

using ‹s ⊆ t› by (simp only: set_rev_mp)

then have "f x ∈ f ` t"

by (rule imageI)

with ‹y = f x› show "y ∈ f ` t"

by (rule ssubst)

qed

section ‹2ª demostración›

lemma

assumes "s ⊆ t"

shows "f ` s ⊆ f ` t"

proof

fix y

assume "y ∈ f ` s"

then show "y ∈ f ` t"

proof

fix x

assume "y = f x"

assume "x ∈ s"

then have "x ∈ t"

using ‹s ⊆ t› by (simp only: set_rev_mp)

then have "f x ∈ f ` t"

by simp

with ‹y = f x› show "y ∈ f ` t"

by simp

qed

section ‹3ª demostración›

lemma

assumes "s ⊆ t"

shows "f ` s ⊆ f ` t"

using assms

by blast

section ‹4ª demostración›

lemma

assumes "s ⊆ t"

shows "f ` s ⊆ f ` t"

using assms

by (simp only: image_mono)

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="lean"> (o <pre lang="isar">) y otra con </pre>

[/expand]