Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-18 12:55 202ac15b

View on Github →

refactor(analysis/topology/topological_space): simplify proof of nhds_supr using Galois connection

Estimated changes

added theorem gc_nhds
added theorem nhds_Sup
added theorem nhds_bot
modified theorem nhds_mono
modified theorem nhds_supr
added theorem pure_le_nhds
deleted theorem return_le_nhds
deleted theorem sup_eq_generate_from
deleted theorem supr_eq_generate_from