Skip to content

Trait Suggestion: Long rays/lines S38, S39, S153 are Cozero complemented P61 #1047

@Moniker1998

Description

@Moniker1998

Trait Suggestion

Long rays/lines S38, S39, S153 are Cozero complemented P61, but this fact is not known to pi-Base today:
link to pi-Base 1
link to pi-Base 2
link to pi-Base 3

Proof/References

Even continuous function $f:X\to \mathbb{R}$ is eventually constant. If $U\subseteq X$ is a cozero-set, then either $U$ is bounded from above, or $U$ contains all values larger than $x$ for some $x\in X$.

In $U$ is bounded from above, say $U\subseteq \{y\in X : y < x\}$, then since $\{y\in X : y < x\}$ is homeomorphic to a subspace of $\mathbb{R}$, its cozero complemented, so there is open $V\subseteq \{y\in X : y < x\}$ disjoint from $U$ such that $U\cup V$ is dense in $\{y\in X : y < x\}$. If $V_0 = V\cup \{y\in X : y > x\}$ then $U, V_0$ are disjoint cozero sets and $U\cup V_0$ is dense in $X$.

If $U$ contains $\{y\in X : y > x\}$, let $U_0 = U\cap \{y\in X : y < x\}$ and find open $V\subseteq \{y\in X : y < x\}$ disjoint from $U_0$ such that $U_0\cup V$ is dense in $\{y\in X : y < x\}$. Then $U, V$ are disjoint cozero sets and $U\cup V$ is dense in $X$.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions