Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-26 01:05 e8da5f21

View on Github →

chore(topology/basic): backport another generalization to Sort* (#18660)

Generalize is_closed_Union to Sort*.
Drop is_open_Inter_prop and is_closed_Union_prop.

Estimated changes

Modified src/topology/basic.lean

modified theorem is_closed_Union

deleted theorem is_closed_Union_prop

deleted theorem is_open_Inter_prop