is_open_bInter_finset

Stream: Is there code for X?

[Moritz Doll]

Is there a version of docs#is_clopen_bInter_finset for is_open?

[Adam Topaz]

docs#is_open_bInter I think?

[Adam Topaz]

Or do you really need a finest version?

[Moritz Doll]

yes, I need it forfinset

[Adam Topaz]

You could combine it with docs#set.finite.of_finset

[Moritz Doll]

ah, cool. Thanks

[Adam Topaz]

Or rather docs#finset.finite_to_set

[Moritz Doll]

this did the job in the end: refine is_open_bInter (to_finite _) _, since it is not obvious, should we add this as a new lemma?

[Eric Wieser]

Can you give the lean version of the statement that you're asking for?

[Moritz Doll]

I haven't checked it in Lean, but it should be this

lemma is_open_bInter_finset {α β : Type*} [topological_space α] {s : finset β} {f : β → set α}
  (h : ∀ i ∈ s, is_open (f i)) :
  is_open (⋂ i ∈ s, f i) := is_open_bInter (to_finite _) h

[Moritz Doll]

but Adam's answer helped me to get a solution, so the only (if any) question would be whether this lemma should be in mathlib

[Eric Wieser]

IMO this is worth a lemma in mathlib, because the term mode proof you gave is about ∈ ↑s not ∈ s

[Yaël Dillies]

The problem is that we have many lemmas that are about either set.finite or finset, but not the other one to match, and that seems to work fine precisely because a ∈ ↑s ↔ a ∈ s. Further, this lemma is not an equality, so you can't rewrite with it and the syntactical difference won't matter.

[Moritz Doll]

I have no strong opinion, aside from my general view that I rather have (slightly) redundant lemmas, so that if you don't know that certain things are definitionally equal you still find a lemma that applies to your situation.