Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Since the proposition that every class has at most one tight apartness is equivalent to excluded middle (this is found at https://martinescardo.github.io/TypeTopology/Apartness.Properties.html#At-Most-One-Tight-Apartness-on-Cantor-gives-WLPO-implies-LPO and https://us.metamath.org/ileuni/exmidmotap.html ), it is not correct to speak of “the apartness” of a local ring. Negated equality would also be an apartness.
kingdon
1 to 2 of 2