From: Enrico Tassi Date: Tue, 13 Oct 2009 09:36:39 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~3326 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3e068a777bc4bda55d3c7eedc2eb8368e8acb6da;p=helm.git ... --- diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index e6caecc63..a38e2eec7 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -122,11 +122,11 @@ are part of the standard library of Matita. These notions come with some standard notation attached to them: -- A ∪ B `A \cup B` -- A ∩ B `A \cap B` -- A ≬ B `A \between B` -- x ∈ A `x \in A` -- Ω^A, that is the type of the subsets of A, `\Omega ^ A` +- A ∪ B can be typed with `A \cup B` +- A ∩ B can be typed with `A \cap B` +- A ≬ B can be typed with `A \between B` +- x ∈ A can be typed with `x \in A` +- Ω^A, that is the type of the subsets of A, can be typed with `\Omega ^ A` The `include` command tells Matita to load a part of the library, in particular the part that we will use can be loaded as follows: