case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ IsOpen ((fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U)
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
⊢ ∀ (s : Set C(α, γ)), s ∈ {m | ∃ s x u x, m = CompactOpen.gen s u} → IsOpen ((fun x => comp x.snd x.fst) ⁻¹' s)
rintro M ⟨K, hK, U, hU, rfl⟩
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ IsOpen fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ IsOpen ((fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U)
conv =>
  congr
  rw [CompactOpen.gen, preimage_setOf_eq]
  ext; dsimp [setOf]
  rw [image_comp, image_subset_iff]
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ ∀ (x : C(α, β) × C(β, γ)),
    (x ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) → ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ x ∈ t
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ IsOpen fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
rw [isOpen_iff_forall_mem_open]
case intro.intro.intro.intro.mk
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
⊢ ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ (φ₀, ψ₀) ∈ t
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ ∀ (x : C(α, β) × C(β, γ)),
    (x ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) → ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ x ∈ t
rintro ⟨φ₀, ψ₀⟩ H
case intro.intro.intro.intro.mk.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ (φ₀, ψ₀) ∈ t
case intro.intro.intro.intro.mk
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
⊢ ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ (φ₀, ψ₀) ∈ t
obtain ⟨L, hL, hKL, hLU⟩ := exists_compact_between (hK.image φ₀.2) (hU.preimage ψ₀.2) H
case intro.intro.intro.intro.mk.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U} ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧
    IsOpen ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}) ∧
      (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
case intro.intro.intro.intro.mk.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ (φ₀, ψ₀) ∈ t
use { φ : C(α, β) | φ '' K ⊆ interior L } ×ˢ { ψ : C(β, γ) | ψ '' L ⊆ U }
case intro.intro.intro.intro.mk.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ IsOpen ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}) ∧ (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
case intro.intro.intro.intro.mk.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U} ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧
    IsOpen ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}) ∧
      (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
use fun ⟨φ, ψ⟩ ⟨(hφ : φ '' K ⊆ interior L), hψ⟩ =>
  subset_trans hφ (interior_subset.trans <| image_subset_iff.mp hψ)
case intro.intro.intro.intro.mk.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
case intro.intro.intro.intro.mk.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ IsOpen ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}) ∧ (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
use (ContinuousMap.isOpen_gen hK isOpen_interior).prod (ContinuousMap.isOpen_gen hL hU)
no goals
case intro.intro.intro.intro.mk.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
exact mem_prod.mpr ⟨hKL, image_subset_iff.mpr hLU⟩