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

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

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

theory Imagen_inversa_de_la_imagen
imports Main
begin

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

end

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

theory Imagen_de_la_union
imports Main
begin

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

end

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

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

theory Imagen_inversa_de_la_interseccion
imports Main
begin

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

end

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

theory Union_con_interseccion_general
imports Main
begin

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

end

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α : Type}
variable (A B : ℕ → Set α)

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
by sorry

theory Interseccion_de_intersecciones
imports Main
begin

lemma "(⋂ i ∈ I. A i ∩ B i) = (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"
sorry

end

import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Tactic

open Set

variable {α : Type}
variable (s : Set α)
variable (A : ℕ → Set α)

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

theory Distributiva_de_la_interseccion_respecto_de_la_union_general
imports Main
begin

lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))"
sorry

end

import Mathlib.Algebra.Ring.Parity
import Mathlib.Tactic

open Nat

def Primos      : Set ℕ := {n | Nat.Prime n}
def MayoresQue2 : Set ℕ := {n | n > 2}
def Impares     : Set ℕ := {n | ¬Even n}

example : Primos ∩ MayoresQue2 ⊆ Impares :=
by sorry

theory Interseccion_de_los_primos_y_los_mayores_que_dos
imports Main "HOL-Number_Theory.Number_Theory"
begin

definition primos :: "nat set" where
  "primos = {n ∈ ℕ . prime n}"

definition mayoresQue2 :: "nat set" where
  "mayoresQue2 = {n ∈ ℕ . n > 2}"

definition impares :: "nat set" where
  "impares = {n ∈ ℕ . ¬ even n}"

lemma "primos ∩ mayoresQue2 ⊆ impares"
oops

end