s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)

Author: jaalonso

README.org

@@ -188,4 +188,5 @@ usaba Lean3 en lugar de Lean4.
 + V16 [[./textos/El_limite_de_u_es_a_syss_el_de_u-a_es_0.md][El límite de u es a syss el de u-a es 0]] (En [[./src/El_limite_de_u_es_a_syss_el_de_u-a_es_0.lean][Lean]] y en [[./thy/El_limite_de_u_es_a_syss_el_de_u-a_es_0.thy][Isabelle]]).
 + S17 [[./textos/Producto_de_sucesiones_convergentes_a_cero.md][Si uₙ y vₙ convergen a 0, entonces uₙvₙ converge a 0]] (En [[./src/Producto_de_sucesiones_convergentes_a_cero.lean][Lean]] y en [[./thy/Producto_de_sucesiones_convergentes_a_cero.thy][Isabelle]]).
 + L19 [[~/alonso/estudio/Calculemus2/textos/Teorema_del_emparedado.md][Teorema del emparedado]] (En [[~/alonso/estudio/Calculemus2/src/Teorema_del_emparedado.lean][Lean]] y en [[~/alonso/estudio/Calculemus2/thy/Teorema_del_emparedado.thy][Isabelle]]).
-+ M20 [[./textos/Propiedad_de_monotonia_de_la_interseccion.md][Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u.]] (En [[./src/Propiedad_de_monotonia_de_la_interseccion.lean][Lean]] y en [[./thy//Propiedad_de_monotonia_de_la_interseccion.thy][Isabelle]]).
++ M20 [[./textos/Propiedad_de_monotonia_de_la_interseccion.md][Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u]] (En [[./src/Propiedad_de_monotonia_de_la_interseccion.lean][Lean]] y en [[./thy//Propiedad_de_monotonia_de_la_interseccion.thy][Isabelle]]).
++ X21 [[./textos/Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.md][s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)]] (En [[./src/Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.lean][Lean]] y en [[./thy/Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.thy][Isabelle]]).

src/Propiedad_de_monotonia_de_la_interseccion.lean

@@ -0,0 +1,142 @@
+-- Propiedad_de_monotonia_de_la_interseccion.lean
+-- Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u.
+-- José A. Alonso Jiménez <https://jaalonso.github.io>
+-- Sevilla, 20-febrero-2024
+-- ---------------------------------------------------------------------
+
+-- ---------------------------------------------------------------------
+-- Demostrar que si
+--    s ⊆ t
+-- entonces
+--    s ∩ u ⊆ t ∩ u
+-- ----------------------------------------------------------------------
+
+-- Demostración en lenguaje natural
+-- ================================
+
+-- Sea x ∈ s ∩ u. Entonces, se tiene que
+--   x ∈ s                                                           (1)
+--   x ∈ u                                                           (2)
+-- De (1) y s ⊆ t, se tiene que
+--   x ∈ t                                                           (3)
+-- De (3) y (2) se tiene que
+--   x ∈ t ∩ u
+-- que es lo que teníamos que demostrar.
+
+-- Demostraciones con Lean4
+-- ========================
+
+import Mathlib.Data.Set.Basic
+import Mathlib.Tactic
+
+open Set
+
+variable {α : Type}
+variable (s t u : Set α)
+
+-- 1ª demostración
+-- ===============
+
+example
+  (h : s ⊆ t)
+  : s ∩ u ⊆ t ∩ u :=
+by
+  rw [subset_def]
+  -- ⊢ ∀ (x : α), x ∈ s ∩ u → x ∈ t ∩ u
+  intros x h1
+  -- x : α
+  -- h1 : x ∈ s ∩ u
+  -- ⊢ x ∈ t ∩ u
+  rcases h1 with ⟨xs, xu⟩
+  -- xs : x ∈ s
+  -- xu : x ∈ u
+  constructor
+  . -- ⊢ x ∈ t
+    rw [subset_def] at h
+    -- h : ∀ (x : α), x ∈ s → x ∈ t
+    apply h
+    -- ⊢ x ∈ s
+    exact xs
+  . -- ⊢ x ∈ u
+    exact xu
+
+-- 2ª demostración
+-- ===============
+
+example
+  (h : s ⊆ t)
+  : s ∩ u ⊆ t ∩ u :=
+by
+  rw [subset_def]
+  -- ⊢ ∀ (x : α), x ∈ s ∩ u → x ∈ t ∩ u
+  rintro x ⟨xs, xu⟩
+  -- x : α
+  -- xs : x ∈ s
+  -- xu : x ∈ u
+  rw [subset_def] at h
+  -- h : ∀ (x : α), x ∈ s → x ∈ t
+  exact ⟨h x xs, xu⟩
+
+-- 3ª demostración
+-- ===============
+
+example
+  (h : s ⊆ t)
+  : s ∩ u ⊆ t ∩ u :=
+by
+  simp only [subset_def]
+  -- ⊢ ∀ (x : α), x ∈ s ∩ u → x ∈ t ∩ u
+  rintro x ⟨xs, xu⟩
+  -- x : α
+  -- xs : x ∈ s
+  -- xu : x ∈ u
+  rw [subset_def] at h
+  -- h : ∀ (x : α), x ∈ s → x ∈ t
+  exact ⟨h _ xs, xu⟩
+
+-- 4ª demostración
+-- ===============
+
+example
+  (h : s ⊆ t)
+  : s ∩ u ⊆ t ∩ u :=
+by
+  intros x xsu
+  -- x : α
+  -- xsu : x ∈ s ∩ u
+  -- ⊢ x ∈ t ∩ u
+  exact ⟨h xsu.1, xsu.2⟩
+
+-- 5ª demostración
+-- ===============
+
+example
+  (h : s ⊆ t)
+  : s ∩ u ⊆ t ∩ u :=
+by
+  rintro x ⟨xs, xu⟩
+  -- xs : x ∈ s
+  -- xu : x ∈ u
+  -- ⊢ x ∈ t ∩ u
+  exact ⟨h xs, xu⟩
+
+-- 6ª demostración
+-- ===============
+
+example
+  (h : s ⊆ t)
+  : s ∩ u ⊆ t ∩ u :=
+  fun _ ⟨xs, xu⟩ ↦  ⟨h xs, xu⟩
+
+-- 7ª demostración
+-- ===============
+
+example
+  (h : s ⊆ t)
+  : s ∩ u ⊆ t ∩ u :=
+  inter_subset_inter_left u h
+
+-- Lema usado
+-- ==========
+
+-- #check (inter_subset_inter_left u : s ⊆ t → s ∩ u ⊆ t ∩ u)

src/Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.lean

@@ -0,0 +1,119 @@
+-- Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.lean
+-- s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)
+-- José A. Alonso Jiménez <https://jaalonso.github.io>
+-- Sevilla, 21-febrero-2024
+-- ---------------------------------------------------------------------
+
+-- ---------------------------------------------------------------------
+-- Demostrar que
+--    s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)
+-- ----------------------------------------------------------------------
+
+-- Demostración en lenguaje natural
+-- ================================
+
+-- Sea x ∈ s ∩ (t ∪ u). Entonces se tiene que
+--    x ∈ s                                                          (1)
+--    x ∈ t ∪ u                                                      (2)
+-- La relación (2) da lugar a dos casos.
+--
+-- Caso 1: Supongamos que x ∈ t. Entonces, por (1), x ∈ s ∩ t y, por
+-- tanto, x ∈ (s ∩ t) ∪ (s ∩ u).
+--
+-- Caso 2: Supongamos que x ∈ u. Entonces, por (1), x ∈ s ∩ u y, por
+-- tanto, x ∈ (s ∩ t) ∪ (s ∩ u).
+
+-- Demostraciones con Lean4
+-- ========================
+
+import Mathlib.Data.Set.Basic
+import Mathlib.Tactic
+
+open Set
+
+variable {α : Type}
+variable (s t u : Set α)
+
+-- 1ª demostración
+-- ===============
+
+example :
+  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
+by
+  intros x hx
+  -- x : α
+  -- hx : x ∈ s ∩ (t ∪ u)
+  -- ⊢ x ∈ s ∩ t ∪ s ∩ u
+  rcases hx with ⟨hxs, hxtu⟩
+  -- hxs : x ∈ s
+  -- hxtu : x ∈ t ∪ u
+  rcases hxtu with (hxt | hxu)
+  . -- hxt : x ∈ t
+    left
+    -- ⊢ x ∈ s ∩ t
+    constructor
+    . -- ⊢ x ∈ s
+      exact hxs
+    . -- hxt : x ∈ t
+      exact hxt
+  . -- hxu : x ∈ u
+    right
+    -- ⊢ x ∈ s ∩ u
+    constructor
+    . -- ⊢ x ∈ s
+      exact hxs
+    . -- ⊢ x ∈ u
+      exact hxu
+
+-- 2ª demostración
+-- ===============
+
+example :
+  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
+by
+  rintro x ⟨hxs, hxt | hxu⟩
+  -- x : α
+  -- hxs : x ∈ s
+  -- ⊢ x ∈ s ∩ t ∪ s ∩ u
+  . -- hxt : x ∈ t
+    left
+    -- ⊢ x ∈ s ∩ t
+    exact ⟨hxs, hxt⟩
+  . -- hxu : x ∈ u
+    right
+    -- ⊢ x ∈ s ∩ u
+    exact ⟨hxs, hxu⟩
+
+-- 3ª demostración
+-- ===============
+
+example :
+  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
+by
+  rintro x ⟨hxs, hxt | hxu⟩
+  -- x : α
+  -- hxs : x ∈ s
+  -- ⊢ x ∈ s ∩ t ∪ s ∩ u
+  . -- hxt : x ∈ t
+    exact Or.inl ⟨hxs, hxt⟩
+  . -- hxu : x ∈ u
+    exact Or.inr ⟨hxs, hxu⟩
+
+-- 4ª demostración
+-- ===============
+
+example :
+  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
+by
+  intro x hx
+  -- x : α
+  -- hx : x ∈ s ∩ (t ∪ u)
+  -- ⊢ x ∈ s ∩ t ∪ s ∩ u
+  aesop
+
+-- 5ª demostración
+-- ===============
+
+example :
+  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
+by rw [inter_union_distrib_left]