Theorem map_nhds_induced_eq
Modification history
2021-02-22 14:12
src/topology/order.lean
refactor(order/filter,topology): review API (#6347) …
Modified map_nhds_induced_eqView on Github →2019-11-12 11:23
src/topology/order.lean
style(*): use notation `𝓝` for `nhds` (#1582) …
Modified map_nhds_induced_eqView on Github →2019-03-08 08:46
src/topology/order.lean
feat(*): has_mem (set α) (filter α) (#799)
Modified map_nhds_induced_eqView on Github →2019-03-03 19:05
src/topology/constructions.lean
chore(topology): Splits topology.basic and topology.continuity (#785) …
Modified map_nhds_induced_eqView on Github →2019-01-18 13:26
src/topology/continuity.lean
refactor(topology): topological_space.induced resembles set.image; second_countable_topology on subtypes; simplify filter.map_comap
Modified map_nhds_induced_eqView on Github →2017-08-10 16:36
topology/continuity.lean
construct reals as complete, linear ordered field
Modified map_nhds_induced_eqView on Github →2017-07-23 18:29
topology/continuity.lean
refactor(*): use 'lemma' iff statement is private
Modified map_nhds_induced_eqView on Github →