lemma placement in mathlib PR

Stream: new members

[Calle Sönne]

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]

for the first question, separation imports subset_properties

[Calle Sönne]

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