Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-18 12:55 6cab92ee

View on Github →

refactor(analysis/topology/topological_space): derive complete lattice structure from Galois insertion

Estimated changes

Modified analysis/topology/continuity.lean

deleted theorem coinduced_compose

deleted theorem coinduced_id

deleted theorem induced_compose

deleted theorem induced_id

Modified analysis/topology/topological_space.lean

added theorem coinduced_compose

added theorem coinduced_id

added theorem generate_from_le_iff_subset_is_open

added def gi_generate_from

added theorem induced_compose

added theorem induced_id

added theorem is_open_fold

added theorem is_open_top

added theorem mk_of_closure_sets

Modified analysis/topology/uniform_space.lean

Modified order/galois_connection.lean

added theorem galois_insertion.l_u_eq