Commit 2020-08-12 10:41 bfcf6400
View on Github →feat(topology/opens): open_embedding_of_le (#3597)
Add lemma open_embedding_of_le {U V : opens α} (i : U ≤ V) : open_embedding (set.inclusion i)
.
Also, I was finding it quite inconvenient to have x ∈ U
for U : opens X
being unrelated to x ∈ (U : set X)
. I propose we just add the simp lemmas in this PR that unfold to the set-level membership operation.
(I'd be happy to go the other way if someone has a strong opinion here; just that we pick a simp normal form for talking about membership and inclusion of opens.)