Theorems · Theorem · general topology

Topology.IsCoinducing.image_connectedComponent

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsCoinducing f →
    (∀ (y : β), IsConnected (f ⁻¹' {y})) → ∀ (a : α), f '' connectedComponent a = connectedComponent (f a)

Defined in

Mathlib.Topology.Connected.Clopen

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace