Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-23 11:55 313f36d4

View on Github →

feat(order/filter/lift): replace some implications with iffs (#16452)

Estimated changes

Modified src/order/filter/lift.lean

modified theorem filter.le_lift'

modified theorem filter.le_lift

modified theorem filter.mem_lift'_sets

modified theorem filter.principal_le_lift'

added theorem filter.sInter_lift'_sets

added theorem filter.sInter_lift_sets

Modified src/topology/basic.lean

Modified src/topology/uniform_space/basic.lean

Modified src/topology/uniform_space/cauchy.lean

Modified src/topology/uniform_space/completion.lean

Modified src/topology/uniform_space/uniform_embedding.lean