Theorems · Definition · general topology

LocallyConstant.indicator

{X : Type u_1} →
  [inst : TopologicalSpace X] →
    {R : Type u_5} → [Zero R] → {U : Set X} → LocallyConstant X R → IsClopen U → LocallyConstant X R

Given a clopen set U and a locally constant function f, LocallyConstant.indicator returns the locally constant function that is f on U and 0 otherwise.

Defined in

Mathlib.Topology.LocallyConstant.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceZero