From 3e068a777bc4bda55d3c7eedc2eb8368e8acb6da Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Oct 2009 09:36:39 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/topology/igft.ma | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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: -- 2.39.2