Theorems · Theorem · general topology

preimage_nhds_within_coinduced

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {X : α → β} {s : Set β} {t : Set α} {a : α},
  a ∈ t → IsOpen t → s ∈ nhds (X a) → X ⁻¹' s ∈ nhds a

Defined in

Mathlib.Topology.NhdsWithin

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace