Skip to main content

Demostraciones de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]"


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

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

import Mathlib.Data.Set.Function

open Set

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

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

y la siguiente teoría de Isabelle/HOL:

theory Union_con_la_imagen_inversa
imports Main
begin

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

end

Read more…

Demostraciones de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​"


Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ∩ v = f[s ∩ f⁻¹[v]] \]

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 : Set α)
variable (v : Set β)

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

y la siguiente teoría de Isabelle/HOL:

theory Interseccion_con_la_imagen_inversa
imports Main
begin

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

end

Read more…

Demostraciones de "f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v"


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

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 : Set α)
variable (v : Set β)

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

y la siguiente teoría de Isabelle/HOL:

theory Union_con_la_imagen
imports Main
begin

lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v"
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
import Mathlib.Tactic

open Set

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

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

y la siguiente teoría de Isabelle/HOL:

theory Interseccion_con_la_imagen
imports Main
begin

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

end

Read more…

Demostraciones de "f[s] \ f[t] ⊆ f[s \ t]"


Demostrar con Lean4 y con Isabelle/HOL que \[f[s] \setminus f[t] ⊆ f[s \setminus 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 : f '' s \ f '' t  f '' (s \ t) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_diferencia_de_conjuntos
imports Main
begin

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

end

Read more…

Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]


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

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

import Mathlib.Data.Set.Function

open Set Function

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

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

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_interseccion_de_aplicaciones_inyectivas
imports Main
begin

lemma
  assumes "inj f"
  shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"
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
import Mathlib.Tactic

open Set

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

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

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_interseccion
imports Main
begin

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"
sorry

end

Read more…

Demostraciones de "f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]​"


Demostrar con Lean4 y con Isabelle/HOL que \[f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]\]

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

import Mathlib.Data.Set.Function

open Set

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

example : f ⁻¹' (A  B) = f ⁻¹' A  f ⁻¹' B :=
by sorry

y la siguiente teoría de IsabelleHOL:

theory Imagen_inversa_de_la_union
imports Main
begin

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

end

Read more…

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…