Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-18 12:55 f9434fa1

View on Github →

refactor(order/filter): derive complete lattice structure from Galois insertion

Estimated changes

Modified analysis/topology/uniform_space.lean

Modified order/filter.lean

added theorem filter.Sup_sets_eq

added theorem filter.bot_sets_eq

added def filter.generate

added theorem filter.generate_Union

added theorem filter.generate_empty

added inductive filter.generate_sets

added theorem filter.generate_union

added theorem filter.generate_univ

added def filter.gi_generate

modified theorem filter.mem_Sup_sets

modified theorem filter.mem_supr_sets

added theorem filter.mem_top_sets

deleted theorem filter.mem_top_sets_iff

added theorem filter.mem_top_sets_iff_forall

added theorem filter.mk_of_closure_sets

modified theorem filter.principal_empty

modified theorem filter.principal_univ

added theorem filter.sets_iff_generate

added theorem filter.sup_sets_eq

added def lattice.complete_lattice.copy