LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$T_{0}$ , $T_{1}$ , and Hausdorffness are hereditary

Statement

The properties $T_{0}$ , $T_{1}$ , and Hausdorffness are hereditary in the sense of Hereditary, open-hereditary and closed-hereditary properties of topological spaces.

Facts & Assumptions

Given: A subspace $S$ of a space $X$ carrying one of the stated properties.

[F1]

An open set of $S$ is $S \cap U$ for an open set $U$ of $X$ (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[F2]

$T_{0}$ distinguishes a distinct pair by one open set, $T_{1}$ separates each point from the other by an open set, and Hausdorffness separates a distinct pair by disjoint open sets ( $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

Proof

technique · direct

1.1F1F2

Let $x, y \in S$ be distinct. If $X$ is $T_{0}$ , choose an open $U \subseteq X$ containing exactly one of $x, y$ ; then $S \cap U$ does the same in $S$ .

1.2F1F2

If $X$ is $T_{1}$ , apply the preceding trace argument separately to the two open sets supplied by the $T_{1}$ condition, so each of $x, y$ has an open neighbourhood in $S$ missing the other.

1.3F1F2

If $X$ is Hausdorff, choose disjoint open $U, V \subseteq X$ containing $x, y$ respectively; $S \cap U$ and $S \cap V$ are disjoint open neighbourhoods in $S$ .

2.1step 1.1step 1.2step 1.3∎

Since $S$ was arbitrary, each of the three properties is hereditary.

$T_{0}$ , $T_{1}$ , and Hausdorffness are hereditary

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

T0T0​, T1T1​, and Hausdorffness are hereditary

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

$T_{0}$ , $T_{1}$ , and Hausdorffness are hereditary