Theorems · Inductive type · general topology

LocallyConstant

(X : Type u_5) → Type u_6 → [TopologicalSpace X] → Type (max u_5 u_6)

A (bundled) locally constant function from a topological space X to a type Y.

Defined in

Mathlib.Topology.LocallyConstant.Basic

Cited by

227 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

TopologicalSpace