Theorems · Theorem · general topology

ContinuousMap.liftCover_coe

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {ι : Type u_5} {S : ι → Set α}
  {φ : (i : ι) → C(↑(S i), β)}
  {hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩}
  {hS : ∀ (x : α), ∃ i, S i ∈ nhds x} {i : ι} (x : ↑(S i)), (ContinuousMap.liftCover S φ hφ hS) ↑x = (φ i) x

Defined in

Mathlib.Topology.ContinuousMap.Basic

Cited by

2 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace