Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-03 09:55 59629da6

View on Github →

chore(*): rename filter.inhabited_of_mem_sets to nonempty_of_mem_sets (#1943) In other names inhabited means that we have a default element.

Estimated changes

Modified src/analysis/calculus/mean_value.lean

Modified src/order/filter/bases.lean

Modified src/order/filter/basic.lean

deleted theorem filter.inhabited_of_mem_sets

added theorem filter.nonempty_of_mem_sets

Modified src/order/liminf_limsup.lean

Modified src/topology/algebra/ordered.lean

Modified src/topology/dense_embedding.lean

Modified src/topology/metric_space/basic.lean

Modified src/topology/order.lean

Modified src/topology/uniform_space/cauchy.lean

modified def sequentially_complete.seq

Modified src/topology/uniform_space/completion.lean

Modified src/topology/uniform_space/uniform_embedding.lean