Para cualquier conjunto s, s ⊆ s
Demostrar con Lean4 que para cualquier conjunto \(s\), \(s ⊆ s\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable {α : Type _} variable (s : Set α) example : s ⊆ s := by sorry |
Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x) [x ∈ s → × ∈ s] \]
Sea \(x\) tal que
\[ x ∈ s \tag{1} \]
Entonces, por (1), se tiene que
\[ x ∈ s \]
que es lo que teníamos que demostrar.
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 |
import Mathlib.Tactic variable {α : Type _} variable (s : Set α) -- 1ª demostración example : s ⊆ s := by intro x xs exact xs -- 2ª demostración example : s ⊆ s := fun (x : α) (xs : x ∈ s) ↦ xs -- 3ª demostración example : s ⊆ s := fun _ xs ↦ xs -- 4ª demostración example : s ⊆ s := -- by exact? rfl.subset -- 5ª demostración example : s ⊆ s := by rfl |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 27.
