Zulip Chat Archive

Stream: maths

Topic: supr and val


view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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