supr and val

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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