case intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V✝ : Set (β × β)
f : C(α, β)
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : f ∈ CompactOpen.gen K U
V : Set (β × β)
hV₁ : V ∈ 𝓤 β
hV₂ : IsOpen V
hV₃ : ∀ (x : β), x ∈ ↑f '' K → ball x V ⊆ U
⊢ ∃ V, V ∈ 𝓤 β ∧ IsOpen V ∧ compactConvNhd K V f ⊆ CompactOpen.gen K U
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : f ∈ CompactOpen.gen K U
⊢ ∃ V, V ∈ 𝓤 β ∧ IsOpen V ∧ compactConvNhd K V f ⊆ CompactOpen.gen K U
obtain ⟨V, hV₁, hV₂, hV₃⟩ := lebesgue_number_of_compact_open (hK.image f.continuous) hU hf
case intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V✝ : Set (β × β)
f : C(α, β)
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : f ∈ CompactOpen.gen K U
V : Set (β × β)
hV₁ : V ∈ 𝓤 β
hV₂ : IsOpen V
hV₃ : ∀ (x : β), x ∈ ↑f '' K → ball x V ⊆ U
⊢ compactConvNhd K V f ⊆ CompactOpen.gen K U
case intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V✝ : Set (β × β)
f : C(α, β)
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : f ∈ CompactOpen.gen K U
V : Set (β × β)
hV₁ : V ∈ 𝓤 β
hV₂ : IsOpen V
hV₃ : ∀ (x : β), x ∈ ↑f '' K → ball x V ⊆ U
⊢ ∃ V, V ∈ 𝓤 β ∧ IsOpen V ∧ compactConvNhd K V f ⊆ CompactOpen.gen K U
refine' ⟨V, hV₁, hV₂, _⟩
case intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V✝ : Set (β × β)
f : C(α, β)
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : f ∈ CompactOpen.gen K U
V : Set (β × β)
hV₁ : V ∈ 𝓤 β
hV₂ : IsOpen V
hV₃ : ∀ (x : β), x ∈ ↑f '' K → ball x V ⊆ U
g : C(α, β)
hg : g ∈ compactConvNhd K V f
x : α
hx : x ∈ K
⊢ ↑g x ∈ U
case intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V✝ : Set (β × β)
f : C(α, β)
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : f ∈ CompactOpen.gen K U
V : Set (β × β)
hV₁ : V ∈ 𝓤 β
hV₂ : IsOpen V
hV₃ : ∀ (x : β), x ∈ ↑f '' K → ball x V ⊆ U
⊢ compactConvNhd K V f ⊆ CompactOpen.gen K U
rintro g hg _ ⟨x, hx, rfl⟩
no goals
case intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V✝ : Set (β × β)
f : C(α, β)
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : f ∈ CompactOpen.gen K U
V : Set (β × β)
hV₁ : V ∈ 𝓤 β
hV₂ : IsOpen V
hV₃ : ∀ (x : β), x ∈ ↑f '' K → ball x V ⊆ U
g : C(α, β)
hg : g ∈ compactConvNhd K V f
x : α
hx : x ∈ K
⊢ ↑g x ∈ U
exact hV₃ (f x) ⟨x, hx, rfl⟩ (hg x hx)