cursolean2026/Curso2026/Conjuntos.lean

import Mathlib.Tactic
/-!

# Conjuntos en Lean

En Lean los conjuntos son siempre homogéneos, es decir: todos sus elementos tienen el mismo tipo.
Para un tipo  `X : Type`, el tipo de los subconjuntos de `X` se llama `Set X`.

Un objeto del tipo `Set X` se puede interpretar de tres formas distintas
1) Un conjunto cuyos elementos tienen tipo `X`
2) Un subconjunto de  `X`;
3) Una función de `X` a `Prop` (enviando los elementos del conjunto a `True` y los demás a `False`)

Notar que `X` es un tipo, pero un conjunto `A` es un término de tipo `Set X`.
Es decir `a : A` no tiene sentido, ya que el tipo de `a` sería `X`.
Lo que tiene sentido es  `a : X` y `a ∈ A`.
`a ∈ A` es cierto o falso, así que el tipo de  `a ∈ A` es `Prop`.

-/


open Set  -- así podemos usar cosas como `univ` en lugar de `Set.univ`


-- por definición, siempre es falso que un elemento pertenezca al vacío
lemma vacio_defin {X : Type} : (∅ : Set X) = {x : X | False} := by
  rfl  -- la táctica `rfl` comprueba que una igualdad se cumple por definición

-- el subconjunto total, es decir, el formado por todos los elementos de `X` se llama `univ`.
-- por definición, todos los elementos de tipo `X` pertenecen a `univ`
lemma total_defin {X : Type} : (univ : Set X) = {x : X | True} := by
  rfl
-- por definición, un elemento está en la intersección de dos conjuntos si y sólo si
-- está en ambos
lemma inter_defin {X : Type} (A B : Set X) : A ∩ B = {x: X | x ∈ A ∧ x ∈ B} := by
  rfl
-- por definición, el complementario de un conjunto está formado por los elementos que no
-- le pertenecen ( el símbolo ᶜ se consigue con \^c )
lemma compl_defin {X : Type} (A : Set X) : Aᶜ = {x : X | x ∉ A} := by
  rfl
-- el complemento del total es el vacío
lemma compl_total {X : Type} : (univ : Set X)ᶜ = ∅  := by
  simp  -- la táctica `simp` simplifica (usando resultados anteriores o en la biblioteca)



-- un conjunto `A` es el vacío si y solo si es falso que cualquier
-- elemento le pertenezca
lemma conjunto_vacio_sii_todo_elemento_no {X : Type} (A : Set X) : A = ∅ ↔ ∀ x : X, ¬(x ∈ A) := by
  constructor
  · intro h x
    rw [h]
    change ¬False  -- la táctica `change` cambia el objetivo por algo que sea igual por definición
    simp
  · intro h
    ext x
    constructor
    · intro hx
      specialize h x
      simp
      exact h hx
    · intro h
      cases h

-- dos conjuntos son disjuntos si y solo si uno está contenido en el complemento del otro:
lemma disjuntos_sii_contenido_en_complemento {X : Type} (A B : Set X):
A ∩ B =  ∅ ↔ A ⊆ Bᶜ := by
  rw [conjunto_vacio_sii_todo_elemento_no]
  constructor
  · intro h x hxA
    simp
    intro hxB
    apply h x
    constructor
    · exact hxA
    · exact hxB
  · intro h x hxAB
    choose hxA hxB using hxAB
    specialize h hxA
    apply h
    exact hxB

/-

## Uniones e intersecciones de familias

Fijado un tipo `X`, si tenemos dos conjuntos `U` y `V`, las operaciones `∪` y `∩` (\cup y \cap
o \union y \inter respectivamente) operan entre ellos y producen un nuevo conjunto en el mismo tipo.

Sin embargo, a veces queremos tomar la unión o intersección de una familia más amplia de conjuntos.
Es decir, dada una familia `F : Set (Set X)` podemos tomar `⋃₀ F` (\Union\0)  la unión de todos
sus elementos. También podemos tomar `⋂₀ F` ( \Inter\0) la intersección de todos ellos.

Los símbolos `⋃₀` y `⋂₀` son notaciones para las operaciones `sUnion` y `sInter`.
-/

example (X : Type) (F : Set (Set X)) : ⋃₀ F = { x : X | ∃ U ∈ F, x ∈ U} := by
  rfl
example (X : Type) (F : Set (Set X)) (x : X) : x ∈ ⋂₀ F ↔ ∀ U ∈ F, x ∈ U := by
  rfl

-- la union de  de una familia es el complementario de las intersecciones de los complementarios
lemma union_familia_es_complementario_de_interseccion_complementarios
  {X : Type} (F : Set (Set X)) :
    ⋃₀ F = (⋂₀ (compl '' F))ᶜ := by
      -- veremos luego por qué `compl '' F` es el conjunto de los complementarios
  -- por doble contenido. tomamos un elemento arbitrario
  ext x
  constructor
  · intro h
    choose S hSF hxS using h
    intro hneg
    specialize hneg Sᶜ
    have h1 : Sᶜ ∈ compl '' F
    · use S
    specialize hneg h1
    apply hneg
    exact hxS
  · intro h
    simp at h
    choose S hSF hxS using h
    use S






/-
Se pueden definir también conjuntos por extensión, es decir, listando sus elementos.

Esto se hace con la sintaxis `{x1, x2, x3}`. Internamente, estos conjuntos están creados
empezando con un `singleton` (un conjunto que tiene un único elemento), y sobre
ese conjunto ir realizando la operación `insert` (agregar un elemento a un conjunto)

-/



lemma union_familia_dos_conjuntos (X : Type) (A B : Set X) : A ∪ B = ⋃₀ {A,B} := by
  ext x
  constructor
  · intro h
    cases' h with h1 h2
    · use A
      constructor
      · left
        rfl
      · exact h1
    · use B
      constructor
      · right
        rfl
      · exact h2
  · intro h
    choose C hCAB hxC using h
    cases'  hCAB with hCA hCB
    · left
      rw [← hCA]
      exact hxC
    · right
      simp at hCB
      rw [hCB] at hxC
      exact hxC



/-
## Conjuntos y funciones

Si tenemos una función entre dos tipos `f : X → Y`, actúa también sobre los conjuntos.

En particular:

- Dado un `V : Set Y`, la preimagen es `f ⁻¹' V`
- Dado un `U : Set Y`, la imagen es `f '' U`
- La imagen de todo el conjunto es `range f`


Las uniones e interseciones parametrizadas se dan como funciones que devuelven conjuntos.
Es decir, si tenemos alguna función `f : X → Set Y`, tomar todos la unión de todos los conjuntos
de la forma `f x` se hace mediante la expresión `⋃ (x : X), (f x)`. Análogamente para la intersección.

También se puede hacer recorriendo sólo un subconjunto `S` de `X`, escribiendo `⋂ (x : X) (hx : x ∈ S), f x`

-/

example (X Y : Type) (f : X → Y) (V : Set Y) : f ⁻¹' V = {x : X | f x ∈ V} := by
  rfl
example (X Y : Type) (f : X → Y) (U : Set X) : f '' U = {y : Y | ∃ x : X, x ∈ U ∧  f x = y} := by
  rfl
example (X Y : Type) (f : X → Y) (U : Set X) : f '' U = { (f x) | x ∈ U } := by
  rfl

example (X Y : Type) (f : X → Y) : range f = {y : Y | ∃ x : X, f x = y} := by
  rfl
example (X Y : Type) (f : X → Y) : range f = f '' univ := by
  simp

example (X Y : Type) (f : X → Set Y) : ⋃₀ range f = ⋃ (x : X), f x := by
  rfl

example (X Y : Type) (f : X → Set Y) (S : Set X) : (⋂ (x : X) (hx : x ∈ S), f x) = {y : Y | ∀ x ∈ S, y ∈ f  x } := by
  ext y
  simp

-- ### Ejercicios

-- La unión de las imágenes es la imagen de la unión

example (X Y : Type) (f : X → Y) (U V : Set X) : f '' (U  ∪ V ) = (f '' U) ∪ (f '' V ) := by
  sorry
example (X Y : Type) (f : X → Y) (F : Set (Set X)) : f '' ⋃₀ F = ⋃₀ {V : Set Y | ∃ U ∈ F, V = f '' U} := by
  sorry
-- La imagén de la intersección está contenida en intersección de las imágenes

example (X Y : Type) (f : X → Y) (U V : Set X) : f '' (U  ∩ V ) ⊆  (f '' U) ∩  (f '' V ) := by
  sorry
example (X Y : Type) (f : X → Y) (F : Set (Set X)) : f '' ⋂₀ F ⊆ ⋂₀ {V : Set Y | ∃ U ∈ F, V = f '' U} := by
  sorry
-- La intersección de las preimagenes es la preimagen de la intersección

example (X Y : Type) (f : X → Y) (U V : Set Y) : f ⁻¹' (U  ∩ V ) = (f ⁻¹' U) ∩ (f ⁻¹' V )  := by
  sorry


example (X Y : Type) (f : X → Y) (F : Set (Set Y)) : f ⁻¹' (⋂₀ F ) = ⋂ (V : Set Y) (hV: V ∈  F), f ⁻¹' V := by
  sorry
-- La unión de las preimagenes es la imagen de la unión

example (X Y : Type) (f : X → Y) (U V : Set Y) :  f ⁻¹' (U  ∪ V ) = (f ⁻¹' U) ∪ (f ⁻¹' V ) := by
  sorry
example (X Y : Type) (f : X → Y) (F : Set (Set Y)) : f ⁻¹' (⋃₀ F ) = ⋃ (V : Set Y) (hV: V ∈  F), f ⁻¹' V := by
  sorry
/-
Algunas fórmulas con uniones e intersecciones
-/

variables (X : Type) (A B C : Set X)

example : A ∪ A = A := by
  sorry

example : A ∩ A = A := by
  sorry

example : A ∩ ∅ = ∅ := by
  sorry

example : A ∪ univ = univ := by
  sorry

example : A ⊆ B → B ⊆ A → A = B := by
  sorry

example : A ∩ B = B ∩ A := by
  sorry

example : A ∩ (B ∩ C) = (A ∩ B) ∩ C := by
  sorry

example : A ∪ (B ∪ C) = (A ∪ B) ∪ C := by
  sorry

example : A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C) := by
  sorry
example : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := by
  sorry
/-
# Subconjuntos como tipos

Hemos visto que lo que en matemáticas habitualmente llamamos conjuntos, en Lean corresponden a tiposy los subconjuntos de estos tipos son de una naturaleza distinta. Sim embargo, en ocasiones
podemos querer considerar un suconjunto de un tipo, como un tipo en sí mismo (por ejemplo,
para definir una función en él). La forma de hacerlo es definiendo un subconjunto `S`
a un tipo `↥S` (el símbolo ↥ se consigue tecleando \u-| )

Si `S` es un subconjunto del tipo `X`, los objetos de tipo `↥S` constan de dos partes:
- un objeto `x` de tipo `X`
- un objeto `hx` de tipo `x ∈ S` (es decir, una demostración, o garantía de que `x` es un elemento de `S`)

  y se escribe de la forma `⟨x,h⟩` (los símbolos `⟨` y `⟩` se escriben con \< y \>  )

  Si tenemos un objeto `y` de tipo `↥S`, sus dos componentes (el objeto del tipo ambiente, y la
  demostración de que está en el subconjunto), podemos recuperarlas usando `y.1`y `y.2` o con la
  táctica `cases'`.

  Además hay automáticamente una función de `↥S` a `X` (la inclusión). Dado un elemento `x : ↥S`  el correspondiente elemento de `X` se denota con `↑x` (el símbolo ↑ se obtiene con \u- )

-/

-- Ejemplo: construimos la aplicación inclusión entre dos conjuntos encajados.

example (X : Type) (U V : Set X) (h : U ⊆ V) : ∃ i : ↥U → ↥V , ∀ x : U, (x : X) = (i x) := by
  let  i : ↥U → ↥V
  · intro x
    cases' x with x1 x2
    fconstructor
    · use x1
    · apply h x2
  · use i
    intro x
    cases' x with xv xp
    rfl


/-
Así como los conjuntos se pueden definir usando la notación `{x : X | P x}`, los correspondientes
tipos se pueden construir usando `{x : X // P x}`
-/

example (X : Type) (P : X → Prop) : ↥{x : X | P x} = {x : X // P x} := by
  rfl