From e88e55208a612a21e25344df089a77536057bde1 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 7 Mar 2012 11:40:06 +0000 Subject: [PATCH] Titols --- weblib/tutorial/chapter4.ma | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index be8ddaa59..e0d122934 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -1,11 +1,14 @@ -(* In this Chapter we shall develop a naif theory of sets represented as +(* +h1 class="section"Naif Set Theory/h1 +*) +In this Chapter we shall develop a naif theory of sets represented as characteristic predicates over some universe codeA/code, that is as objects of type A→Prop. *) include "basics/types.ma". include "basics/bool.ma". -(**** For instance the empty set is defined by the always function predicate *) +(* For instance the empty set is defined by the always false function: *) definition empty_set ≝ λA:Type[0].λa:A.a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. notation "\emptyv" non associative with precedence 90 for @{'empty_set}. -- 2.39.2