charFn_eq_zero

Mathlib.Topology.LocallyConstant.Algebra

URI: https://scilib.ai/kg/mathlib#LocallyConstant.charFn_eq_zero

English

For Nontrivial Y and IsClopen U, the equality charFn Y hU x = 0 holds precisely when x ∉ U.

Русский

При непустом Y и IsClopen U, равенство charFn Y hU x = 0 происходит тогда, когда x ∉ U.

LaTeX

$$charFn Y hU x = 0 ⇔ x ∉ U$$

Lean4

theorem charFn_eq_zero [Nontrivial Y] (x : X) (hU : IsClopen U) : charFn Y hU x = (0 : Y) ↔ x ∉ U :=
  Set.indicator_eq_zero_iff_notMem _

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru