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

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

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

Read More «Si f es inyectiva, entonces f⁻¹[f[s]​] ⊆ s»

f[s] ⊆ u ↔ s ⊆ f⁻¹[u]

Demostrar con Lean4 que
\[ f[s] ⊆ u ↔ s ⊆ f⁻¹[u] \]

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

Read More «f[s] ⊆ u ↔ s ⊆ f⁻¹[u]»

s ⊆ f⁻¹[f[s]​]

Demostrar 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:

Read More «s ⊆ f⁻¹[f[s]​]»

f[s ∪ t] = f[s] ∪ f[t]

En Lean4, la imagen de un conjunto s por una función f se representa por f '' s; es decir,

Demostrar con Lean4 que

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

Read More «f[s ∪ t] = f[s] ∪ f[t]»

f⁻¹[u ∩ v] = f⁻¹[u] ∩ f⁻¹[v]

En Lean, la imagen inversa de un conjunto s (de elementos de tipo β) por la función f (de tipo α → β) es el conjunto f ⁻¹' s de elementos x (de tipo α) tales que f x ∈ s.

Demostrar con Lean4 que

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

Read More «f⁻¹[u ∩ v] = f⁻¹[u] ∩ f⁻¹[v]»