Theorems · Theorem · general topology

inducing_sigma

∀ {X : Type u} {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] [inst_1 : TopologicalSpace X]
  {f : Sigma σ → X},
  Topology.IsInducing f ↔
    (∀ (i : ι), Topology.IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i

A map defined on a sigma type (a.k.a. the disjoint union of an indexed family of topological spaces) is inducing iff its restriction to each component is inducing and each the image of each component under f can be separated from the images of all other components by an open set.

Defined in

Mathlib.Topology.Constructions

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace