Synthetic_Basis_formed_from_Synthetic_Sub_Basis

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Synthetic_Basis_formed_from_Synthetic_Sub_Basis is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Let $X$ be a set. Let $\SS$ be a synthetic sub-basis on $X$. Define \displaystyle \BB = \set {\bigcap \FF: \FF \subseteq \SS, \text{\FF is finite} } Then $\BB$ is a synthetic basis on $X$.

Why this node was retired

The posted statement is

theorem Synthetic_Basis_formed_from_Synthetic_Sub_Basis {α : Type _} (S : Set (Set α)) : ∃ (t : TopologicalSpace α), True := by sorry

The goal is ∃ (t : TopologicalSpace α), True, witnessed by the indiscrete topology. The sub-basis S never appears in the conclusion, so nothing connects the topology to it.

What a faithful statement would require

The conclusion must assert that the collection of finite intersections of members of S is a basis for the topology generated by S.

No corrected replacement node exists yet.