Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-29 08:21 80f2762c

View on Github →

feat(topology): assorted topological lemmas (#3619) from the sphere eversion project

Estimated changes

Modified src/data/set/basic.lean

added theorem set.union_diff_cancel'

added theorem subtype.preimage_coe_nonempty

Modified src/order/filter/bases.lean

added theorem filter.has_basis.ex_mem

added theorem filter.has_basis.has_basis_self_subset

added theorem filter.has_basis.restrict

added theorem filter.has_basis_iff

Modified src/order/filter/basic.lean

added theorem filter.image_coe_mem_sets

added theorem filter.image_mem_sets

added theorem filter.not_ne_bot

Modified src/topology/basic.lean

added theorem closure_eq_interior_union_frontier

added theorem closure_eq_self_union_frontier

added theorem is_closed_iff_nhds

Modified src/topology/order.lean

added theorem continuous_induced_rng'

Modified src/topology/subset_properties.lean

added def connected_component_in

added theorem connected_space_iff_connected_component

added theorem eq_univ_of_nonempty_clopen

added theorem is_connected_range