Continuity on basic opens

Stream: Is there code for X?

[Justus Springer]

I find it hard to believe that we don't have the following lemma:

import topology.bases

open topological_space

lemma continuous_of_basis_preimage_open {α β : Type*} [topological_space α] [topological_space β]
  (B : set (set β)) (hB : is_topological_basis B) (f : α → β)
  (hf : ∀ s ∈ B, is_open s → is_open (f ⁻¹' s)) :
  continuous f :=
{ is_open_preimage := λ s hs,
begin
  obtain ⟨ι, U, rfl, hU⟩ := hB.open_eq_Union hs,
  rw set.preimage_Union,
  apply is_open_Union,
  intro i,
  exact hf (U i) (hU i) (hB.is_open (hU i)),
end }

Am I just not seeing it?

[Adam Topaz]

I wouldn't be surprised if it's not there... the API for topological bases needs some attention.

[Patrick Massot]

Indeed this thing is defined and not used much. However your statement is needlessly complicated. In assumption hf, the openness condition is automatic:

import topology.bases

open topological_space

lemma continuous_of_basis_preimage_open {α β : Type*} [topological_space α] [topological_space β]
  (B : set (set β)) (hB : is_topological_basis B) (f : α → β)
  (hf : ∀ s ∈ B, is_open (f ⁻¹' s)) :
  continuous f :=
{ is_open_preimage := λ s hs,
begin
  obtain ⟨ι, U, rfl, hU⟩ := hB.open_eq_Union hs,
  rw set.preimage_Union,
  apply is_open_Union,
  exact λ i, hf (U i) (hU i),
end }

[Patrick Massot]

Note that if you want to develop this you should probably try to tie it to our extensive filter library. The reason why this subarea of our topology library is underdeveloped is because the notion of filter bases is so much more useful.

[Yury G. Kudryashov]

Another option is to rewrite on docs#topological_space.is_topological_basis.eq_generate_from (available as B.eq_generate_from), then apply docs#continuous_generated_from

[Justus Springer]

Thanks for your comments! With Yury's proof it gets very trivial. Do you think it would still be worth it having this lemma?

[Justus Springer]

I PR'd it: #9281

[Justus Springer]

But I can close it again if you think it's not worth it.

[Yury G. Kudryashov]

We have lots of short and simple convenience lemmas. This one will be a nice addition to the list.