Theorems · Theorem · general topology

LocallyConstant.charFn_eq_zero

∀ {X : Type u_1} (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : MulZeroOneClass Y] {U : Set X} [Nontrivial Y]
  (x : X) (hU : IsClopen U), (LocallyConstant.charFn Y hU) x = 0 ↔ x ∉ U

Defined in

Mathlib.Topology.LocallyConstant.Algebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMulZeroOneClassNontrivial