diff --git a/Curso2026/Conjuntos.lean b/Curso2026/Conjuntos.lean
new file mode 100644
index 0000000..a0c593b
--- /dev/null
+++ b/Curso2026/Conjuntos.lean
@@ -0,0 +1,312 @@
+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
diff --git a/Curso2026/Proposiciones.lean b/Curso2026/Proposiciones.lean
new file mode 100644
index 0000000..76cc68b
--- /dev/null
+++ b/Curso2026/Proposiciones.lean
@@ -0,0 +1,162 @@
+import Mathlib.Tactic
+/-!
+# Proposiciones en Lean
+
+Una proposición representa una afirmación que puede ser cierta o falsa.
+
+Por ejemplo, `(P : Prop)` quiere decir que con la letra `P` vamos a representar una
+cierta afirmación.
+
+Para una proposición `P`, podemos tener (o no) la certeza de que es cierta, (porque contamos
+  con una demostración de la misma,  o porque la asumimos como hipótesis).
+
+  Esto se escribe como `(h : P)`. Ahí estamos diciendo que h es una demostración de `P`.
+
+
+  # Implicaciones
+
+  Una implicación `P → Q`  (el símbolo → se puede obtener tecleando \to  \->  o \r )
+  representa el hecho de que "si `P` es cierta, entonces `Q` también lo es".
+  También puede interpretarse como una función, que dada una demostración para `P`
+  produce una demostración para `Q`.
+-/
+
+-- Ejemplo: vamos a demostrar un ejemplo muy básico: si sabemos que `P` es cierta
+-- podemos demostrar que `P` es cierta:
+
+-- para ello se puede usar la táctica `exact`
+
+example (P : Prop) (h : P) : P := by
+  exact h
+
+-- Otro ejemplo, si queremos demostrar una implicación, podemos tomar la premisa
+-- como hipótesis, y demostrar la tesis. Para ello se usa la táctica `intro`
+
+example (P Q : Prop) (hq : Q) : P → Q := by
+  intro hp
+  exact hq
+
+-- La táctica `apply`se puede usar cuando tenemos como hipótesis una implicación `h`
+-- que implica nuestro objetivo. Al usarla, el objetivo cambia y pasamos a tener que
+-- demostrar la premisa de `h`
+
+example (P Q : Prop) (hI : P → Q) (hp : P) : Q := by
+  apply hI
+  exact hp
+
+-- La táctica `constructor` divide un objetivo que consiste de dos afirmaciones, en dos
+-- objetivos separados (hay una variante más potente llamada `fconstructor`.)
+
+example (P : Prop) : P ↔ P := by
+  constructor
+  · intro h
+    exact h
+  · intro h
+    exact h
+
+
+-- Sirve tanto para dobles implicaciones como para conjunciones
+
+example (P : Prop) : P → (P ∧ P) := by
+  intro h
+  constructor
+  · exact h
+  · exact h
+
+
+-- Si tenemos que demostrar una disyunción, tenemos que usar `left` o `right` para decidir
+-- cual de los dos lados vamos a demostrar
+
+example (P Q : Prop) : P → P ∨ Q := by
+  intro h
+  left
+  exact h
+
+example (P Q : Prop) : Q → P ∨ Q  := by
+  intro h
+  right
+  exact h
+
+-- Si tenemos una hipótesis que consiste de varias afirmaciones, `cases'` nos la separa en varias
+-- hipótesis. Si la hipótesis es una disyunción, nos separa el objetivo en varios casos
+
+example (P Q : Prop) (h : P ∧ Q) : Q := by
+  cases' h with h1 h2
+  exact h2
+
+example (P Q : Prop) (h : P ∨ Q ) : P ∨ Q := by
+  cases' h with h h
+  · left
+    exact h
+  · right
+    exact h
+
+
+/-
+# Ejercicios
+-/
+
+variable (p q r s : Prop)
+
+/-
+## Demuestra la conmutatividad de ∧ y ∨
+-/
+example : p ∧ q ↔ q ∧ p := by
+  sorry
+example : p ∨ q ↔ q ∨ p := by
+  sorry
+
+
+
+
+
+/-
+## Demuestra la asociatividad de  ∧ y  ∨
+-/
+example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := by
+  sorry
+example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
+  sorry
+
+
+/-
+## Demuestra la distributividad de ∧ respecto de ∨ y viceversa
+p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)
+p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)
+-/
+
+
+/-
+## Demuestra las siguientes propiedades
+
+(p → (q → r)) ↔ (p ∧ q → r)
+((p ∨ q) → r) ↔ (p → r) ∧ (q → r)
+¬(p ∨ q) ↔ ¬p ∧ ¬q
+¬p ∨ ¬q → ¬(p ∧ q)
+¬(p ∧ ¬p)
+p ∧ ¬q → ¬(p → q)
+¬p → (p → q)
+(¬p ∨ q) → (p → q)
+p ∨ false ↔ p
+p ∧ false ↔ false
+(p → q) → (¬q → ¬p)
+-/
+
+/-
+## Algunas demostraciones que requieren razonamiento clásico
+
+Estas demostraciones requieren usar algunas tácticas nuevas:
+
+- `by_contra` asume la negación del objetivo, y tenemos que demostrar una contradicción
+- `by_cases`  h : P crea dos nuevos contextos: uno en el que tenemos que demostrar el objetivo
+  suponiendo P, y otro en el que tenemos que demostrarlo suponiendo ¬ P
+- `push_neg` "mete las negaciones" en una expresión. Por ejemplo cambia ¬ (P ∧ Q) por ¬ P ∨ ¬ Q
+
+(p → r ∨ s) → ((p → r) ∨ (p → s))
+¬(p ∧ q) → ¬p ∨ ¬q
+¬(p → q) → p ∧ ¬q
+(p → q) → (¬p ∨ q)
+(¬q → ¬p) → (p → q)
+p ∨ ¬p
+(((p → q) → p) → p)
+-/