is_closed_prod

Stream: Is there code for X?

[Ashvni Narayanan]

My goal is to show that the product of clopen sets is clopen. As a supporting statement, I need the following :

lemma is_closed_prod {α β : Type*} [topological_space α] [topological_space β] {s : set α}
  {t : set β} (h : is_closed s ∧ is_closed t) : is_closed (set.prod s t) :=

Is this already in mathlib? Thank you!

[Sebastien Gouezel]

It's called is_closed.prod, to make sure that dot notation works fine. I found it using regexp search for is_closed.*prod in vscode

[Eric Wieser]

Lemmas will almost never take P ∧ Q as an assumption unless they live in the and namespace (eg docs#and.elim), which probably thwarted your search

[Ashvni Narayanan]

Thank you!