Formal target: Corpus.PaperWeaklyFirstCountable.existsWeaklyFirstCountableCompactNotFirstCountable

Problem 3 in [Ar2013]: Give an example in ZFC of a weakly first- countable compact Hausdorff space which is not first countable.

Exact formal statement

Exists.{2} fun X =>
  Exists.{1} fun x =>
    And (Corpus.PaperWeaklyFirstCountable.WeaklyFirstCountableTopology.{0} X)
      (And (CompactSpace.{0} X) (And (T2Space.{0} X) (Not (FirstCountableTopology.{0} X))))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record