-
Notifications
You must be signed in to change notification settings - Fork 0
/
La_equipotencia_es_una_relacion_reflexiva.thy
44 lines (35 loc) · 1.34 KB
/
La_equipotencia_es_una_relacion_reflexiva.thy
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
(* La_equipotencia_es_una_relacion_reflexiva.thy
-- La equipotencia es una relación reflexiva.
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 18-junio-2024
-- ------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
-- Dos conjuntos A y B son equipotentes (y se denota por A \<simeq> B) si
-- existe una aplicación biyectiva entre ellos. La equipotencia está
-- definida en Isabelle por
-- definition eqpoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl "\<approx>" 50)
-- where "eqpoll A B \<equiv> \<exists>f. bij_betw f A B"
--
-- Demostrar que la relación de equipotencia es reflexiva.
-- ------------------------------------------------------------------ *)
theory La_equipotencia_es_una_relacion_reflexiva
imports Main "HOL-Library.Equipollence"
begin
(* 1\<ordfeminine> demostración *)
lemma "reflp (\<approx>)"
proof (rule reflpI)
fix x :: "'a set"
have "bij_betw id x x"
by (simp only: bij_betw_id)
then have "\<exists>f. bij_betw f x x"
by (simp only: exI)
then show "x \<approx> x"
by (simp only: eqpoll_def)
qed
(* 2\<ordfeminine> demostración *)
lemma "reflp (\<approx>)"
by (simp only: reflpI eqpoll_refl)
(* 3\<ordfeminine> demostración *)
lemma "reflp (\<approx>)"
by (simp add: reflpI)
end