Skip to main content

Monotonía de la imagen inversa


Demostrar con Lean4 y con Isabelle/HOL que si \(u ⊆ v\), entonces \(f⁻¹[u] ⊆ f⁻¹[v]\).

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

import Mathlib.Data.Set.Function
open Set

variable {α β : Type _}
variable (f : α  β)
variable (u v : Set β)

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

y la siguiente teoría de Isabelle/HOL:

theory Monotonia_de_la_imagen_inversa
imports Main
begin

lemma
  assumes "u ⊆ v"
  shows "f -` u ⊆ f -` v"
sorry

end

Read more…

Monotonía de la imagen de conjuntos


Demostrar con Lean4 y con Isabelle/HOL que si \(s ⊆ t\), entonces \(f[s] ⊆ f[t]\).

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α  β)
variable (s t : Set α)

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

y la siguiente teoría de Isabelle/HOL:

theory Monotonia_de_la_imagen_de_conjuntos
imports Main
begin

lemma
  assumes "s ⊆ t"
  shows "f ` s ⊆ f ` t"
sorry

end

Read more…

Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]​]


Demostrar con Lean4 y con Isabelle/HOL que si \(f\) es suprayectiva, entonces \[ u ⊆ f[f⁻¹[u]] \]

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

import Mathlib.Data.Set.Function
open Set Function
variable {α β : Type _}
variable (f : α  β)
variable (u : Set β)

example
  (h : Surjective f)
  : u  f '' (f⁻¹' u) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_imagen_inversa_de_aplicaciones_suprayectivas
imports Main
begin

lemma
  assumes "surj f"
  shows "u ⊆ f ` (f -` u)"
sorry

end

Read more…

Demostraciones de "f[f⁻¹[u]] ⊆ u"


Demostrar con Lean4 y con Isabelle/HOL que \[ f[f⁻¹[u]] ⊆ u \]

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

import Mathlib.Data.Set.Function
open Set

variable {α β : Type _}
variable (f : α  β)
variable (u : Set β)

example : f '' (f⁻¹' u)  u :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_imagen_inversa
imports Main
begin

lemma "f ` (f -` u) ⊆ u"
sorry

end

Read more…

Si f es inyectiva, entonces f⁻¹[f[s]] ⊆ s


Demostrar con Lean4 y con Isabelle/HOL que si \(f\) es inyectiva, entonces \(f⁻¹[f[s]​] ⊆ s\).

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

import Mathlib.Data.Set.Function
open Set Function
variable {α β : Type _}
variable (f : α  β)
variable (s : Set α)

example
  (h : Injective f)
  : f ⁻¹' (f '' s)  s :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_inversa_de_la_imagen_de_aplicaciones_inyectivas
imports Main
begin

lemma
  assumes "inj f"
  shows "f -` (f ` s) ⊆ s"
sorry

end

Read more…

Demostraciones de "f[s] ⊆ u ↔ s ⊆ f⁻¹[u]"


Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ⊆ u ↔ s ⊆ f⁻¹[u] \]

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

import Mathlib.Data.Set.Function
open Set
variable {α β : Type _}
variable (f : α  β)
variable (s : Set α)
variable (u : Set β)

example : f '' s  u  s  f ⁻¹' u :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Subconjunto_de_la_imagen_inversa
imports Main
begin

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"
sorry

end

Read more…

Demostraciones de "s ⊆ f⁻¹(f(s))"


Demostrar con Lean4 e Isabelle/HOL que si \(s\) es un subconjunto del dominio de la función \(f\), entonces \(s\) está contenido en la imagen inversa de la imagen de \(s\) por \(f\); es decir, \[ s ⊆ f⁻¹[f[s]] \]

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

import Mathlib.Data.Set.Function
open Set
variable {α β : Type _}
variable (f : α  β)
variable (s : Set α)

example : s  f ⁻¹' (f '' s) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_inversa_de_la_imagen
imports Main
begin

lemma "s ⊆ f -` (f ` s)"
sorry

end

Read more…

Demostraciones de "f(s ∪ t) = f(s) ∪ f(t)"


Demostrar con Lean4 y con Isabelle/HOL que \[ f(s ∪ t) = f(s) ∪ f(t) \] Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Set.Function
variable {α β : Type _}
variable (f : α  β)
variable (s t : Set α)
open Set

example : f '' (s  t) = f '' s  f '' t :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_union
imports Main
begin

lemma "f ` (s ∪ t) = f ` s ∪ f ` t"
sorry

end

Read more…

Demostraciones de "f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)"


Demostrar con Lean4 y con Isabelle/HOL que

   f⁻¹(u  v) = f⁻¹(u)  f⁻¹(v)

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

import Mathlib.Data.Set.Function
variable {α β : Type _}
variable (f : α  β)
variable (u v : Set β)
open Set

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

y la siguiente teoría de Iasbelle/HOL:

theory Imagen_inversa_de_la_interseccion
imports Main
begin

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

end

Read more…

Demostraciones de "s ∪ (⋂_i A_i) = ⋂_i (A_i ∪ s)"


Demostrar con Lean4 y con Isabelle/HOL que \[ s ∪ (⋂_i A_i) = ⋂_i (A_i ∪ s) \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s : Set α)
variable (A :   Set α)

example : s  ( i, A i) =  i, (A i  s) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Union_con_interseccion_general
imports Main
begin

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"
sorry

end

Read more…