Theorems · Theorem · general topology

IsLocallyConstant.tfae

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : X → Y),
  [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in nhds x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE

Defined in

Mathlib.Topology.LocallyConstant.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpace