Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-20 08:57 53650a00

View on Github →

feat(*): lemmas about disjoint on sets and filters (#11549)

Estimated changes

Modified src/data/set/function.lean

Modified src/data/set/lattice.lean

added theorem disjoint.ne_of_mem

added theorem set.disjoint_iff_forall_ne

Modified src/order/filter/basic.lean

added theorem filter.disjoint_comap

added theorem filter.disjoint_map

Modified src/topology/basic.lean

added theorem disjoint.closure_left

added theorem disjoint.closure_right