Return to Question

By constructive mathematics in this matter we mean intuitionistic ZF (*).

In the language of locales, the Jordan curve can be defined as $f\colon S^1 \to X$ such that "if $U \cap V = \varnothing$, then $f(U) \cap f(V) = \varnothing$" (coincides with the classical definition for Hausdorff spaces).

So, is Jordan's theorem true for locales in constructive mathematics?

(*) I like Martin-Löf's intuitionistic theory of types more and it seems that in a sense "this is the same question", but I have not studied the type theory systematically yet, so I am formulating the question in a more familiar language.

By constructive mathematics in this matter we mean intuitionistic ZF (*).

In the language of locales, the Jordan curve can be defined as $f\colon S^1 \to X$ such that "if $U \cap V = \varnothing$, then $f(U) \cap f(V) = \varnothing$" (coincides with the classical definition for Hausdorff spaces).

So, is Jordan's theorem true for locales in constructive mathematics?

(*) I like Martin-Löf's intuitionistic theory of types more and it seems that in a sense "this is the same question", but I have not studied the type theory systematically yet, so I am formulating the question in a more familiar language.

By constructive mathematics in this matter we mean intuitionistic ZF (*).

In the language of locales, the Jordan curve can be defined as $f\colon I \to X$ such that "if $U \cap V = \varnothing$, then $f(U) \cap f(V) = \varnothing$" (coincides with the classical definition for Hausdorff spaces).

So, is Jordan's theorem true for locales in constructive mathematics?

(*) I like Martin-Löf's intuitionistic theory of types more and it seems that in a sense "this is the same question", but I have not studied the type theory systematically yet, so I am formulating the question in a more familiar language.

By constructive mathematics in this matter we mean intuitionistic ZF (*).

In the language of locales, the Jordan curve can be defined as $f\colon S^1 \to X$ such that "if $U \cap V = \varnothing$, then $f(U) \cap f(V) = \varnothing$" (coincides with the classical definition for Hausdorff spaces).

So, is Jordan's theorem true for locales in constructive mathematics?

(*) I like Martin-Löf's intuitionistic theory of types more and it seems that in a sense "this is the same question", but I have not studied the type theory systematically yet, so I am formulating the question in a more familiar language.

By constructive mathematics in this matter we mean ZF without the law of the excluded third (*).

In the language of locales, the Jordan curve can be defined as $f\colon I \to X$ such that "if $U \cap V = \varnothing$, then $f(U) \cap f(V) = \varnothing$" (coincides with the classical definition for Hausdorff spaces).

So, is Jordan's theorem true for locales in constructive mathematics?

(*) I like Martin-Löf's intuitionistic theory of types more and it seems that in a sense "this is the same question", but I have not studied the type theory systematically yet, so I am formulating the question in a more familiar language.

By constructive mathematics in this matter we mean intuitionistic ZF (*).

In the language of locales, the Jordan curve can be defined as $f\colon I \to X$ such that "if $U \cap V = \varnothing$, then $f(U) \cap f(V) = \varnothing$" (coincides with the classical definition for Hausdorff spaces).

So, is Jordan's theorem true for locales in constructive mathematics?

(*) I like Martin-Löf's intuitionistic theory of types more and it seems that in a sense "this is the same question", but I have not studied the type theory systematically yet, so I am formulating the question in a more familiar language.