Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-29 23:40 cb7fb9ba

View on Github →

feat(topology): basic setup for measurable spaces

Estimated changes

Created topology/measurable_space.lean

added def is_measurable

added theorem is_measurable_Union

added theorem is_measurable_compl

added theorem is_measurable_empty

added def measurable

added theorem measurable_space.comap_bot

added theorem measurable_space.comap_comp

added theorem measurable_space.comap_id

added theorem measurable_space.comap_le_iff_le_map

added theorem measurable_space.comap_map_le

added theorem measurable_space.comap_mono

added theorem measurable_space.comap_sup

added theorem measurable_space.comap_supr

added theorem measurable_space.gc_comap_map

added theorem measurable_space.le_map_comap

added theorem measurable_space.map_comp

added theorem measurable_space.map_id

added theorem measurable_space.map_inf

added theorem measurable_space.map_infi

added theorem measurable_space.map_mono

added theorem measurable_space.map_top

added theorem measurable_space.monotone_comap

added theorem measurable_space.monotone_map

added structure measurable_space

added theorem measurable_space_eq