search

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 298 forks source link

feat(topology/order): Add closure.mono #19224

Closed mans0954 closed 1 year ago

mans0954 commented 1 year ago

Adds closure.mono which asserts that if t₁ ≤ t₂ for topologies t₁, t₂, then the closure of a set in t₁ will be a subset of the closure of the set in t₂. Analogous to is_open.mono and is_closed.mono.

See discussion

Open in Gitpod

mans0954 commented 1 year ago

I think I'm now meant to create an empty "holding" PR in mathlib4 - but it doesn't seem to be possible to create empty PRs?

j-loreaux commented 1 year ago

You should just close this and PR to mathlib 4 instead. It will be less work for you.

mans0954 commented 1 year ago

You should just close this and PR to mathlib 4 instead. It will be less work for you.

For files that exist in both mathlib and mathlib4 I thought it was mandatory to get the PR merged in mathlib and then forward port to mathlib4?

mans0954 commented 1 year ago

Closing in favour of https://github.com/leanprover-community/mathlib4/pull/5631