Documentation

Mathlib.Topology.Baire.CompleteMetrizable

First Baire theorem #

In this file we prove that a completely metrizable topological space is a Baire space. Since Mathlib does not have the notion of a completely metrizable topological space yet, we state it for a complete uniform space with countably generated uniformity filter.

@[instance 100]

First Baire theorem: a completely metrizable topological space has Baire property.

Since Mathlib does not have the notion of a completely metrizable topological space yet, we state it for a complete uniform space with countably generated uniformity filter.

Equations
  • =