## Stream: new members

### Topic: lemma placement in mathlib PR

#### 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

#### Mario Carneiro (Dec 11 2020 at 11:49):

for the first question, separation imports subset_properties

#### 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