Set is open iff each point has a open neighbourhood containe

Stream: Is there code for X?

[Michael Rothgang]

This is a standard lemma from point-set topology: a subset $s\subseteq X$ of a topological space X is open iff each point x \in x is contained in an open subset of s. I can't find this in mathlib (neither eyeballing, nor apply?/exact?/hint return anything). Did I overlook something?

lemma aux {X : Type*} [TopologicalSpace X] {s : Set X} :
    IsOpen s ↔ ∀ x, x ∈ s → ∃ t : Set X, x ∈ t ∧ t ⊆ s ∧ IsOpen t := by
  constructor
  · intro h x hx
    rcases mem_nhds_iff.mp (h.mem_nhds hx) with ⟨t, hts, htopen, hxt⟩
    use t
  · sorry -- this seems to be missing?

[Michael Rothgang]

I'd be interested both in the backwards direction and the full iff; as you can see, mathlib basically contains the direction $\to$ already.

[Rémy Degenne]

docs#isOpen_iff_forall_mem_open

[Rémy Degenne]

I opened the doc and searched for "isopen iff mem"

[Michael Rothgang]

I wasn't sure what I could search for... thank you for the quick response!

[Patrick Massot]

Probably you don't need this result actually. Open neighborhoods are overrated.

[Kevin Buzzard]

I used this result on Thursday to prove that the sum of two continuous cocycles $G\to A$ was continuous (the target has the discrete topology). I'm wondering what I did wrong now :-) I had to prove $(\phi_1+\phi_2)^{-1}\{m\}$ was open knowing that $\forall t, \phi_1^{-1}\{t\}$ and $\phi_2^{-1}\{t\}$ were open. My proof was to use the above lemma, which gives me some $x$, and then apply the hypotheses to $\phi_1(x)$ and $\phi_2(x)$ and take the intersection.

[Patrick Massot]

#mwe?

[Kevin Buzzard]

import Mathlib.Tactic

variables
  (G : Type) [Group G] [TopologicalSpace G] [TopologicalGroup G]
  (M : Type) [AddCommGroup M]

open TopologicalSpace

def continuous_cocycles : AddSubgroup (G → M) where
  carrier := {φ : G → M | ∀ m : M, IsOpen (φ ⁻¹' {m})}
  add_mem' := by
    intros φ₁ φ₂ h₁ h₂ m
    rw [isOpen_iff_forall_mem_open] -- here
    intro g (hg : φ₁ g + φ₂ g = m)
    specialize h₁ (φ₁ g)
    specialize h₂ (φ₂ g)
    refine ⟨(φ₁ ⁻¹' {φ₁ g}) ∩ (φ₂ ⁻¹' {φ₂ g}), ?_, ?_, ?_⟩
    · intro x
      intro h1
      simp at h1
      simp [h1.1, h1.2, hg]
    · apply IsOpen.inter h₁ h₂
    · aesop
  zero_mem' := sorry
  neg_mem' := sorry

[Michael Rothgang]

Patrick Massot said:

Probably you don't need this result actually. Open neighborhoods are overrated.

I'm using it for this lemma: the interior of a smooth manifold is open.
It allows reducing this to charts nicely. Golfing ideas welcome.

[Anatole Dedecker]

Kevin, I think Patrick was suggesting something along these lines:

import Mathlib.Tactic

variables
  (G : Type) [Group G] [TopologicalSpace G] [TopologicalGroup G]
  (M : Type) [AddCommGroup M]

open TopologicalSpace

def continuous_cocycles : AddSubgroup (G → M) where
  carrier := {φ : G → M | ∀ m : M, IsOpen (φ ⁻¹' {m})}
  add_mem' := by
    intros φ₁ φ₂ h₁ h₂ m
    rw [isOpen_iff_eventually]
    intro g (hg : φ₁ g + φ₂ g = m)
    filter_upwards [(h₁ (φ₁ g)).mem_nhds rfl, (h₂ (φ₂ g)).mem_nhds rfl]
      with x (h1 : _ = _) (h2 : _ = _)
    rwa [← h1, ← h2] at hg
  zero_mem' := sorry
  neg_mem' := sorry

Neighborhoods are not overrated, open ones are. But I get in this case you don't gain a lot.

[Kevin Buzzard]

Oh it's nice to see this technique though! Thanks!

[Patrick Massot]

Anatole is right that I had something like this in mind of course. But why stopping at rw [isOpen_iff_eventually] instead of going all the way to simp only [isOpen_iff_eventually] at *?

import Mathlib.Tactic

variable
  (G : Type) [Group G] [TopologicalSpace G] [TopologicalGroup G]
  (M : Type) [AddCommGroup M]

open TopologicalSpace Topology

def continuous_cocycles : AddSubgroup (G → M) where
  carrier := {φ : G → M | ∀ m : M, IsOpen (φ ⁻¹' {m})}
  add_mem' := by
    intros φ₁ φ₂ h₁ h₂ m
    simp only [isOpen_iff_eventually] at *
    rintro g rfl
    apply (h₁ (φ₁ g) g rfl |>.and <| h₂ (φ₂ g) g rfl).mono
    aesop
  zero_mem' := sorry
  neg_mem' := sorry