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 (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

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

open Set

variable {α : Type}
variable (s t : Set α)

example : (s \\ t) ∪ (t \\ s) = (s ∪ t) \\ (s ∩ t) :=
by sorry

theory Diferencia_de_union_e_interseccion
imports Main
begin

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"
oops

end

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

open Set

variable {α : Type}
variable (s t u : Set α)

example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):=
by sorry

theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union_2
imports Main
begin

lemma "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)"
oops

end

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s t u : Set α)

example :
  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
by sorry

theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union
imports Main
begin

lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"
oops

end

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s t u : Set α)

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
by sorry

theory Propiedad_de_monotonia_de_la_interseccion
imports Main
begin

lemma
  assumes "s ⊆ t"
  shows   "s ∩ u ⊆ t ∩ u"
oops

end