Unión con intersección general
Demostrar con Lean4 que \[ s ∪ (⋂_i A_i) = ⋂_i (A_i ∪ s) \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α : Type} variable (s : Set α) variable (A : ℕ → Set α) example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) := by sorry
1. Demostración en lenguaje natural
Tenemos que demostrar que para todo \(x\), \[ x ∈ s ∪ ⋂_i A_i ↔ x ∈ ⋂_i (A i ∪ s) \] Lo haremos mediante la siguiente cadena de equivalencias \begin{align} x ∈ s ∪ ⋂_i A_i &↔ x ∈ s ∨ x ∈ ⋂_i A_i \newline &↔ x ∈ s ∨ (∀ i)[x ∈ A_i] \newline &↔ (∀ i)[x ∈ s ∨ x ∈ A_i] \newline &↔ (∀ i)[x ∈ A_i ∨ x ∈ s] \newline &↔ (∀ i)[x ∈ A_i ∪ s] \newline &↔ x ∈ ⋂_i (A_i ∪ s) \end{align}
2. Demostraciones con Lean4
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α : Type} variable (s : Set α) variable (A : ℕ → Set α) -- 1ª demostración -- =============== example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) := by ext x -- x : α -- ⊢ x ∈ s ∪ ⋂ (i : ℕ), A i ↔ x ∈ ⋂ (i : ℕ), A i ∪ s calc x ∈ s ∪ ⋂ i, A i ↔ x ∈ s ∨ x ∈ ⋂ i, A i := by simp only [mem_union] _ ↔ x ∈ s ∨ ∀ i, x ∈ A i := by simp only [mem_iInter] _ ↔ ∀ i, x ∈ s ∨ x ∈ A i := by simp only [forall_or_left] _ ↔ ∀ i, x ∈ A i ∨ x ∈ s := by simp only [or_comm] _ ↔ ∀ i, x ∈ A i ∪ s := by simp only [mem_union] _ ↔ x ∈ ⋂ i, A i ∪ s := by simp only [mem_iInter] -- 2ª demostración -- =============== example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) := by ext x -- x : α -- ⊢ x ∈ s ∪ ⋂ (i : ℕ), A i ↔ x ∈ ⋂ (i : ℕ), A i ∪ s simp only [mem_union, mem_iInter] -- ⊢ (x ∈ s ∨ ∀ (i : ℕ), x ∈ A i) ↔ ∀ (i : ℕ), x ∈ A i ∨ x ∈ s constructor . -- ⊢ (x ∈ s ∨ ∀ (i : ℕ), x ∈ A i) → ∀ (i : ℕ), x ∈ A i ∨ x ∈ s intros h i -- h : x ∈ s ∨ ∀ (i : ℕ), x ∈ A i -- i : ℕ -- ⊢ x ∈ A i ∨ x ∈ s rcases h with (xs | xAi) . -- xs : x ∈ s right -- ⊢ x ∈ s exact xs . -- xAi : ∀ (i : ℕ), x ∈ A i left -- ⊢ x ∈ A i exact xAi i . -- ⊢ (∀ (i : ℕ), x ∈ A i ∨ x ∈ s) → x ∈ s ∨ ∀ (i : ℕ), x ∈ A i intro h -- h : ∀ (i : ℕ), x ∈ A i ∨ x ∈ s -- ⊢ x ∈ s ∨ ∀ (i : ℕ), x ∈ A i by_cases cxs : x ∈ s . -- cxs : x ∈ s left -- ⊢ x ∈ s exact cxs . -- cns : ¬x ∈ s right -- ⊢ ∀ (i : ℕ), x ∈ A i intro i -- i : ℕ -- ⊢ x ∈ A i rcases h i with (xAi | xs) . -- ⊢ x ∈ A i exact xAi . -- xs : x ∈ s exact absurd xs cxs -- 3ª demostración -- =============== example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) := by ext x -- x : α -- ⊢ x ∈ s ∪ ⋂ (i : ℕ), A i ↔ x ∈ ⋂ (i : ℕ), A i ∪ s simp only [mem_union, mem_iInter] -- ⊢ (x ∈ s ∨ ∀ (i : ℕ), x ∈ A i) ↔ ∀ (i : ℕ), x ∈ A i ∨ x ∈ s constructor . -- ⊢ (x ∈ s ∨ ∀ (i : ℕ), x ∈ A i) → ∀ (i : ℕ), x ∈ A i ∨ x ∈ s rintro (xs | xI) i . -- xs : x ∈ s -- i : ℕ -- ⊢ x ∈ A i ∨ x ∈ s right -- ⊢ x ∈ s exact xs . -- xI : ∀ (i : ℕ), x ∈ A i -- i : ℕ -- ⊢ x ∈ A i ∨ x ∈ s left -- ⊢ x ∈ A i exact xI i . -- ⊢ (∀ (i : ℕ), x ∈ A i ∨ x ∈ s) → x ∈ s ∨ ∀ (i : ℕ), x ∈ A i intro h -- h : ∀ (i : ℕ), x ∈ A i ∨ x ∈ s -- ⊢ x ∈ s ∨ ∀ (i : ℕ), x ∈ A i by_cases cxs : x ∈ s . -- cxs : x ∈ s left -- ⊢ x ∈ s exact cxs . -- cxs : ¬x ∈ s right -- ⊢ ∀ (i : ℕ), x ∈ A i intro i -- i : ℕ -- ⊢ x ∈ A i cases h i . -- h : x ∈ A i assumption . -- h : x ∈ s contradiction -- Lemas usados -- ============ -- variable (x : α) -- variable (s t : Set α) -- variable (a b q : Prop) -- variable (p : ℕ → Prop) -- #check (absurd : a → ¬a → b) -- #check (forall_or_left : (∀ x, q ∨ p x) ↔ q ∨ ∀ x, p x) -- #check (mem_iInter : x ∈ ⋂ i, A i ↔ ∀ i, x ∈ A i) -- #check (mem_union x a b : x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t) -- #check (or_comm : a ∨ b ↔ b ∨ a)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
theory Union_con_interseccion_general imports Main begin (* 1ª demostración *) lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)" proof (rule equalityI) show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)" proof (rule subsetI) fix x assume "x ∈ s ∪ (⋂ i ∈ I. A i)" then show "x ∈ (⋂ i ∈ I. A i ∪ s)" proof (rule UnE) assume "x ∈ s" show "x ∈ (⋂ i ∈ I. A i ∪ s)" proof (rule INT_I) fix i assume "i ∈ I" show "x ∈ A i ∪ s" using ‹x ∈ s› by (rule UnI2) qed next assume h1 : "x ∈ (⋂ i ∈ I. A i)" show "x ∈ (⋂ i ∈ I. A i ∪ s)" proof (rule INT_I) fix i assume "i ∈ I" with h1 have "x ∈ A i" by (rule INT_D) then show "x ∈ A i ∪ s" by (rule UnI1) qed qed qed next show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)" proof (rule subsetI) fix x assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)" show "x ∈ s ∪ (⋂ i ∈ I. A i)" proof (cases "x ∈ s") assume "x ∈ s" then show "x ∈ s ∪ (⋂ i ∈ I. A i)" by (rule UnI1) next assume "x ∉ s" have "x ∈ (⋂ i ∈ I. A i)" proof (rule INT_I) fix i assume "i ∈ I" with h2 have "x ∈ A i ∪ s" by (rule INT_D) then show "x ∈ A i" proof (rule UnE) assume "x ∈ A i" then show "x ∈ A i" by this next assume "x ∈ s" with ‹x ∉ s› show "x ∈ A i" by (rule notE) qed qed then show "x ∈ s ∪ (⋂ i ∈ I. A i)" by (rule UnI2) qed qed qed (* 2ª demostración *) lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)" proof show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)" proof fix x assume "x ∈ s ∪ (⋂ i ∈ I. A i)" then show "x ∈ (⋂ i ∈ I. A i ∪ s)" proof assume "x ∈ s" show "x ∈ (⋂ i ∈ I. A i ∪ s)" proof fix i assume "i ∈ I" show "x ∈ A i ∪ s" using ‹x ∈ s› by simp qed next assume h1 : "x ∈ (⋂ i ∈ I. A i)" show "x ∈ (⋂ i ∈ I. A i ∪ s)" proof fix i assume "i ∈ I" with h1 have "x ∈ A i" by simp then show "x ∈ A i ∪ s" by simp qed qed qed next show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)" proof fix x assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)" show "x ∈ s ∪ (⋂ i ∈ I. A i)" proof (cases "x ∈ s") assume "x ∈ s" then show "x ∈ s ∪ (⋂ i ∈ I. A i)" by simp next assume "x ∉ s" have "x ∈ (⋂ i ∈ I. A i)" proof fix i assume "i ∈ I" with h2 have "x ∈ A i ∪ s" by (rule INT_D) then show "x ∈ A i" proof assume "x ∈ A i" then show "x ∈ A i" by this next assume "x ∈ s" with ‹x ∉ s› show "x ∈ A i" by simp qed qed then show "x ∈ s ∪ (⋂ i ∈ I. A i)" by simp qed qed qed (* 3ª demostración *) lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)" proof show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)" proof fix x assume "x ∈ s ∪ (⋂ i ∈ I. A i)" then show "x ∈ (⋂ i ∈ I. A i ∪ s)" proof assume "x ∈ s" then show "x ∈ (⋂ i ∈ I. A i ∪ s)" by simp next assume "x ∈ (⋂ i ∈ I. A i)" then show "x ∈ (⋂ i ∈ I. A i ∪ s)" by simp qed qed next show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)" proof fix x assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)" show "x ∈ s ∪ (⋂ i ∈ I. A i)" proof (cases "x ∈ s") assume "x ∈ s" then show "x ∈ s ∪ (⋂ i ∈ I. A i)" by simp next assume "x ∉ s" then show "x ∈ s ∪ (⋂ i ∈ I. A i)" using h2 by simp qed qed qed (* 4ª demostración *) lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)" proof show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)" proof fix x assume "x ∈ s ∪ (⋂ i ∈ I. A i)" then show "x ∈ (⋂ i ∈ I. A i ∪ s)" proof assume "x ∈ s" then show ?thesis by simp next assume "x ∈ (⋂ i ∈ I. A i)" then show ?thesis by simp qed qed next show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)" proof fix x assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)" show "x ∈ s ∪ (⋂ i ∈ I. A i)" proof (cases "x ∈ s") case True then show ?thesis by simp next case False then show ?thesis using h2 by simp qed qed qed (* 5ª demostración *) lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)" by auto end