Unión de los conjuntos de los pares e impares
Los conjuntos de los números naturales, de los pares y de los impares se definen por
|
1 2 3 |
def naturales : set ℕ := {n | true} def pares : set ℕ := {n | even n} def impares : set ℕ := {n | ¬ even n} |
Demostrar que
|
1 |
pares ∪ impares = naturales |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import data.nat.parity import data.set.basic import tactic open set def naturales : set ℕ := {n | true} def pares : set ℕ := {n | even n} def impares : set ℕ := {n | ¬ even n} example : pares ∪ impares = naturales := sorry |
Soluciones con Lean
|
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 |
import data.nat.parity import data.set.basic import tactic open set def naturales : set ℕ := {n | true} def pares : set ℕ := {n | even n} def impares : set ℕ := {n | ¬ even n} -- 1ª demostración -- =============== example : pares ∪ impares = naturales := begin unfold pares impares naturales, ext n, simp, apply classical.em, end -- 2ª demostración -- =============== example : pares ∪ impares = naturales := begin unfold pares impares naturales, ext n, finish, end -- 3ª demostración -- =============== example : pares ∪ impares = naturales := by finish [pares, impares, naturales, ext_iff] |
Soluciones 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 |
theory Union_de_pares_e_impares imports Main begin definition naturales :: "nat set" where "naturales = {n∈ℕ . True}" definition pares :: "nat set" where "pares = {n∈ℕ . even n}" definition impares :: "nat set" where "impares = {n∈ℕ . ¬ even n}" section ‹1ª demostración› lemma "pares ∪ impares = naturales" proof - have "∀ n ∈ ℕ . even n ∨ ¬ even n ⟷ True" by simp then have "{n ∈ ℕ. even n} ∪ {n ∈ ℕ. ¬ even n} = {n ∈ ℕ. True}" by auto then show "pares ∪ impares = naturales" by (simp add: naturales_def pares_def impares_def) qed section ‹2ª demostración› lemma "pares ∪ impares = naturales" unfolding naturales_def pares_def impares_def by auto end |
Nuevas soluciones
- En los comentarios se pueden escribir nuevas soluciones.
- El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>
