Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-02 11:47 3f66b3a2

View on Github →

feat(analysis/topology/continuity): generalized tube lemma and some corollaries

Estimated changes

Modified analysis/topology/continuity.lean

added theorem closed_of_compact

added theorem compact_compact_separated

added theorem continuous_swap

added theorem diagonal_eq_range_diagonal_map

added theorem generalized_tube_lemma

added theorem nhds_contain_boxes.comm

added theorem nhds_contain_boxes.symm

added def nhds_contain_boxes

added theorem nhds_contain_boxes_of_compact

added theorem nhds_contain_boxes_of_singleton

added theorem prod_subset_compl_diagonal_iff_disjoint

Modified analysis/topology/topological_space.lean

added theorem is_open_bInter

added theorem is_open_bUnion