Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-04 05:36 afbf47d5

View on Github →

feat(data/, order/) supporting lemmas for characterising well-founded complete lattices (#5446)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.eq_singleton_iff_nonempty_unique_mem

added theorem finset.not_nonempty_iff_eq_empty

Modified src/data/finset/lattice.lean

added theorem finset.inf_eq_Inf

added theorem finset.sup_closed_of_sup_closed

added theorem finset.sup_eq_Sup

Modified src/data/set/basic.lean

added theorem set.eq_singleton_iff_nonempty_unique_mem

Modified src/data/set/finite.lean

added theorem set.finite.preimage_embedding

Modified src/order/complete_lattice.lean

added theorem eq_singleton_bot_of_Sup_eq_bot_of_nonempty

added theorem eq_singleton_top_of_Inf_eq_top_of_nonempty

Modified src/order/rel_iso.lean

added theorem rel_hom.map_inf

added theorem rel_hom.map_sup