Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u
Demostrar con Lean4 que «Si \(s ⊆ t\), entonces \(s ∩ u ⊆ t ∩ u\)».
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
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 |
1. Demostración en lenguaje natural
Sea \(x ∈ s ∩ u\). Entonces, se tiene que
\begin{align}
&x ∈ s \tag{1} \\
&x ∈ u \tag{2}
\end{align}
De (1) y \(s ⊆ t\), se tiene que
\[ x ∈ t \tag{3} \]
De (3) y (2) se tiene que
\[ x ∈ t ∩ u \]
que es lo que teníamos que demostrar.
2. Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 |
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) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 |
theory Propiedad_de_monotonia_de_la_interseccion imports Main begin (* 1ª solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" proof (rule subsetI) fix x assume hx: "x ∈ s ∩ u" have xs: "x ∈ s" using hx by (simp only: IntD1) then have xt: "x ∈ t" using assms by (simp only: subset_eq) have xu: "x ∈ u" using hx by (simp only: IntD2) show "x ∈ t ∩ u" using xt xu by (simp only: Int_iff) qed (* 2 solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" proof fix x assume hx: "x ∈ s ∩ u" have xs: "x ∈ s" using hx by simp then have xt: "x ∈ t" using assms by auto have xu: "x ∈ u" using hx by simp show "x ∈ t ∩ u" using xt xu by simp qed (* 3ª solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" using assms by auto (* 4ª solución *) lemma "s ⊆ t ⟹ s ∩ u ⊆ t ∩ u" by auto end |
