Zulip Chat Archive

Stream: new members

Topic: lemma placement in mathlib PR


view this post on Zulip Calle Sönne (Dec 11 2020 at 11:46):

Hello, I am preparing a PR to mathlib with a bunch of topology lemmas that I have proven whilst doing some work on some Profinite spaces stuff. I am wondering about where to place some of these lemmas. Mostly I am unsure of what to do when I have lemmas that require imports from multiple files. An example:
I have this lemma:

lemma connected_component_Inter {α : Type*} [topological_space α] [t2_space α] [compact_space α] :
   x : α, connected_component x =  Z : {Z : set α // is_clopen Z  x  Z}, Z :=

My first guess would be to place this in the subset_properties.lean file with the other connected component stuff, but this requires the t2 hypothesis and so I would need to import an additional file which I am unsure if its a good idea to do. Should I make a completely new file just to place this lemma?
A similar situation is with:

lemma continuous_on.preimage_clopen_of_clopen {α β: Type*} [topological_space α] [topological_space β]
  {f : α  β} {s : set α} {t : set β} (hf : continuous_on f s) (hs : is_clopen s)
  (ht : is_clopen t) : is_clopen (s  f⁻¹' t) :=

Again, if I place this in the continuous_on file it would require more imports so I am not sure where to place this

view this post on Zulip Mario Carneiro (Dec 11 2020 at 11:49):

for the first question, separation imports subset_properties

view this post on Zulip Calle Sönne (Dec 11 2020 at 11:55):

Mario Carneiro said:

for the first question, separation imports subset_properties

yeah I did notice that, but it felt wierd to place this lemma in separation (if thats what you were implying I should do).


Last updated: May 13 2021 at 21:12 UTC