Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-22 12:31 e0abdabe

View on Github →

feat(topology/topological_space): add countablility and separability axioms for topological spaces

Estimated changes

Modified data/set/countable.lean

modified theorem set.countable_empty

added theorem set.countable_set_of_finite_subset

modified theorem set.countable_singleton

Modified data/set/lattice.lean

added theorem bind_def

added def disjoint

added theorem disjoint_bot_left

added theorem disjoint_bot_right

added theorem disjoint_symm

added theorem fmap_eq_image

added theorem image_Union

added theorem mem_seq_iff

added theorem monotone_preimage

added theorem preimage_Union

added theorem preimage_sUnion

added theorem set.Inter_neg

added theorem set.Inter_pos

added theorem set.Inter_univ

added theorem set.Union_empty

added theorem set.Union_neg

added theorem set.Union_pos

deleted theorem set.bind_def

deleted def set.disjoint

deleted theorem set.disjoint_bot_left

deleted theorem set.disjoint_bot_right

deleted theorem set.disjoint_symm

deleted theorem set.fmap_eq_image

deleted theorem set.image_Union

deleted theorem set.mem_seq_iff

deleted theorem set.monotone_preimage

deleted theorem set.preimage_Union

deleted theorem set.preimage_sUnion

added theorem set.sdiff_empty

added theorem set.sdiff_eq:

added theorem set.union_sdiff_left

added theorem set.union_sdiff_right

deleted theorem set.univ_subtype

added theorem univ_subtype

Modified order/complete_lattice.lean

added theorem lattice.infi_neg

added theorem lattice.infi_pos

added theorem lattice.supr_neg

added theorem lattice.supr_pos

Modified topology/measurable_space.lean

Modified topology/outer_measure.lean

deleted theorem Inter_neg

deleted theorem Inter_pos

deleted theorem Inter_univ

deleted theorem Union_empty

deleted theorem Union_neg

deleted theorem Union_pos

deleted theorem sdiff_empty

deleted theorem sdiff_eq:

deleted theorem union_sdiff_left

deleted theorem union_sdiff_right

Modified topology/topological_space.lean

added theorem is_open_sInter

added theorem topological_space.is_open_generated_countable_inter

Modified topology/topological_structures.lean

deleted theorem infi_neg

deleted theorem infi_pos

deleted theorem supr_neg

deleted theorem supr_pos