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

theory Imagen_de_la_diferencia_de_conjuntos
imports Main
begin

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

end

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

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

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

theory Imagen_de_la_interseccion
imports Main
begin

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

end

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

theory Imagen_inversa_de_la_union
imports Main
begin

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

end

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

theory Monotonia_de_la_imagen_inversa
imports Main
begin

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

end

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

theory Monotonia_de_la_imagen_de_conjuntos
imports Main
begin

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

end

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

theory Imagen_de_imagen_inversa_de_aplicaciones_suprayectivas
imports Main
begin

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

end

import Mathlib.Data.Set.Function
open Set

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

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

theory Imagen_de_la_imagen_inversa
imports Main
begin

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

end

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

theory Imagen_inversa_de_la_imagen_de_aplicaciones_inyectivas
imports Main
begin

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

end

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

theory Subconjunto_de_la_imagen_inversa
imports Main
begin

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

end