Theorems · Definition · general topology

extendFrom

{X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → Set X → (X → Y) → X → Y

Extend a function from a set A. The resulting function g is such that at any x₀, if f converges to some y as x tends to x₀ within A, then g x₀ is defined to be one of these y. Else, g x₀ could be anything.

Defined in

Mathlib.Topology.ExtendFrom

Cited by

15 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace