mathlib3
e8da5f21 - chore(topology/basic): backport another generalization to `Sort*` (#18660)

Commit

2 years ago

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`.

Author

urkud

Parents

55d771df

mathlib3 e8da5f21 - chore(topology/basic): backport another generalization to `Sort*` (#18660)

mathlib3
e8da5f21 - chore(topology/basic): backport another generalization to `Sort*` (#18660)