Second-countability helpers #
Point-set topology preliminaries for the Poincaré–Volterra lemma
(Rado/Topology/PoincareVolterra.lean):
- a compact set in a locally second-countable space is second countable;
- a countable cover by second-countable open sets gives second countability
(set-of-sets version of
secondCountableTopology_of_countable_cover); - ccc: a second-countable space has no uncountable pairwise-disjoint family of nonempty open sets;
- countable-branching reachability is countable.
All statements are pure topology, independent of the rest of the development.
theorem
Rado.IsCompact.secondCountableTopology
{Z : Type u_1}
[TopologicalSpace Z]
{K : Set Z}
(hK : IsCompact K)
(hloc : ∀ z ∈ K, ∃ (U : Set Z), z ∈ U ∧ IsOpen U ∧ SecondCountableTopology ↑U)
:
A compact set each of whose points has a second-countable open neighbourhood is second countable in the subspace topology (cover by finitely many).
theorem
Rado.secondCountableTopology_of_countable_setCover
{Z : Type u_1}
[TopologicalSpace Z]
{𝒰 : Set (Set Z)}
(hct : 𝒰.Countable)
(ho : ∀ U ∈ 𝒰, IsOpen U)
(hsc : ∀ U ∈ 𝒰, SecondCountableTopology ↑U)
(hcov : ⋃₀ 𝒰 = Set.univ)
:
A countable family of second-countable open sets covering Z makes Z
second countable.
theorem
Rado.countable_of_pairwiseDisjoint_isOpen
{Z : Type u_1}
[TopologicalSpace Z]
[SecondCountableTopology Z]
{𝒰 : Set (Set Z)}
(ho : ∀ U ∈ 𝒰, IsOpen U)
(hne : ∀ U ∈ 𝒰, U.Nonempty)
(hdisj : 𝒰.PairwiseDisjoint id)
:
ccc: in a second-countable space, every pairwise-disjoint family of nonempty open sets is countable.