Theorems · Inductive type · measure theory

SecondCountableTopologyEither

(α : Type u_6) → (β : Type u_7) → [TopologicalSpace α] → [TopologicalSpace β] → Prop

The typeclass SecondCountableTopologyEither α β registers the fact that at least one of the two spaces has second countable topology. This is the right assumption to ensure that continuous maps from α to β are strongly measurable.

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Cited by

117 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace