Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 14:15 a5807271

View on Github →

chore(topology/omega_complete_partial_order): golf (#11250)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.set_of_bijective

Modified src/order/omega_complete_partial_order.lean

added theorem complete_lattice.inf_continuous'

Modified src/topology/omega_complete_partial_order.lean

modified theorem Scott.is_open_sUnion