Ir al contenido principal

Publicaciones sobre Imagen

Canal RSS (Imagen, es)

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

Fundamentos/Funciones

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

Leer más…

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

Fundamentos/Funciones

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

Leer más…