diff --git a/type.md b/type.md new file mode 100644 index 00000000..a4279446 --- /dev/null +++ b/type.md @@ -0,0 +1,30 @@ +--- +up: +tags: + - s/maths/topologie +aliases: +--- + +> [!definition] Définition +> Soit $V = \{ x_1, \dots, x_{n} \}$ un ensemble (fini) de symboles de variables +> Un **type** en les variables $V$ est un ensemble de formules dont les variables libres appartiennent à $V$ de la forme : +> $\operatorname{tp}_{A}(a) = \{f \mid A \models f(a_1, \dots, a_{n}) \}$ l'ensemble des formules satisfaites dans $A$ +> où $a = (a_1, \dots, a_{n})$ et où $A$ est une structure pour la signature donnée $a_1, \dots, a_{n} \in A$ +> +> > [!info] Cas particulier important +> > pour $n = 0$ et $V = \emptyset$ +> > on notera plutôt $\operatorname{Th}(A) = \{ f \mid A \models f \}$ l'ensemble des énoncés vrais dans $A$, i.e la théorie de $A$ +^definition + +> [!definition] Ensemble des types +> Soit $\mathcal{F}_{n}$ l'ensemble des formules à variables libres dans $\{ x_1, \dots, x_{n} \}$ +> On note $\mathscr{S}_{n} \in \mathcal{P}(\mathcal{P}(\mathcal{F}_{n}))$ l'ensemble de tous les types en $\{ x_1, \dots, x_{n} \}$ +> - i $\mathscr{S}_{0}$ est l'ensemble de toutes les théories +> +> > [!info]- Topologie sur $\mathscr{S}_{n}$ +> > $f \in \mathcal{F}_{n}$ +> > $\{ t \in \mathscr{S}_{n} \mid f \in t \} =$ +# Propriétés + +# Exemples +