## Stream: maths

### Topic: supr and val

#### Kevin Buzzard (Dec 30 2019 at 09:10):

I was hoping this would be rfl:

import topology.opens

open topological_space

lemma what_is_this_called {X Y : Type*} [topological_space X] [topological_space Y] {f : X → Y}
(hf : continuous f) {γ : Type*}
(ι : γ → opens Y) :
(⨆ (j : γ), hf.comap (ι j)).val = ⋃ (j : γ), f ⁻¹' (ι j).val :=
begin
sorry
end


This is surely much easier than I am making it...

#### Kevin Buzzard (Dec 30 2019 at 09:47):

opens.Sup_s is helpful!

lemma what_is_this_called {X Y : Type*} [topological_space X] [topological_space Y] {f : X → Y}
(hf : continuous f) {γ : Type*}
(ι : γ → opens Y) :
(⨆ (j : γ), hf.comap (ι j)).val = ⋃ (j : γ), f ⁻¹' (ι j).val :=
begin
unfold lattice.supr,
rw opens.Sup_s,
ext x,
split,
rintro ⟨V, HV, H⟩,
use V,
existsi _,
exact H,
convert HV,
ext Z,
split,
rintro ⟨i, rfl⟩,
split,
split,
use i,
refl,
rintro ⟨_, ⟨i, rfl⟩, rfl⟩,
use i,
refl,
rintro ⟨_, ⟨j, rfl⟩, h3⟩,
rw set.mem_sUnion,
use f ⁻¹' (ι j).val,
existsi _,
exact h3,
existsi hf.comap (ι j),
split,
use j,
refl,
end


#### Chris Hughes (Dec 30 2019 at 09:54):

The lemma opens.supr_val seems to be missing

lemma opens.supr_val {X γ : Type*} [topological_space X] (ι : γ → opens X) :
(⨆ i, ι i).val = ⨆ i, (ι i).val :=
@galois_connection.l_supr (opens X) (set X) _ _ _ (subtype.val : opens X → set X)
opens.interior opens.gc _

lemma what_is_this_called {X Y : Type*} [topological_space X] [topological_space Y] {f : X → Y}
(hf : continuous f) {γ : Type*}
(ι : γ → opens Y) :
(⨆ (j : γ), hf.comap (ι j)).val = ⋃ (j : γ), f ⁻¹' (ι j).val :=
begin
simp [set.ext_iff, opens.supr_val, continuous.comap],
end


#### Chris Hughes (Dec 30 2019 at 09:54):

Also, things like continuous.mem_comap would be good simp lemmas.

Last updated: May 06 2021 at 18:20 UTC