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