Theorems · Theorem · general topology

ContinuousOn.image_connectedComponentIn_subset

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α} {a : α},
  ContinuousOn f s → a ∈ s → f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a)

Defined in

Mathlib.Topology.Connected.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace