Efektywna polska przestrzeń

W logice matematycznej efektywna polska przestrzeń to kompletna rozdzielna przestrzeń metryczna , która ma obliczalną prezentację. Takie przestrzenie są badane w efektywnej opisowej teorii mnogości iw analizie konstruktywnej . W szczególności standardowe przykłady przestrzeni polskich, takie jak linia rzeczywista , zbiór Cantora i przestrzeń Baire'a , są efektywnymi przestrzeniami polskimi.

Definicja

₀ Efektywna polska przestrzeń to kompletna rozdzielna przestrzeń metryczna X z metryką d taka, że ​​istnieje przeliczalny gęsty zbiór C = ( do , do ₁ , ...), który tworzy następujące dwie relacje na ${\ displaystyle \ mathbb {N } ^{4}}$ obliczalny (Moschovakis 2009:96-7):

${\ Displaystyle P (i, j, k, m) \ równoważnik \ lewo \ {d (c_ {i },c_{j})\leq {\frac {m}{k+1}}\right\}}$

${\ Displaystyle Q (i, j, k, m) \ równoważnik \ lewo \ {d (c_ {i}, c_ {j}) <{\ Frac {m} {k + 1}} \ prawo \} }$

•   Yiannis N. Moschovakis , 2009, Descriptive Set Theory , wydanie 2, Amerykańskie Towarzystwo Matematyczne. ISBN 0-8218-4813-5