charFn_eq_one

Mathlib.Topology.LocallyConstant.Algebra

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

English

For Nontrivial Y, and a clopen set U, the equality charFn Y hU x = 1 holds precisely when x ∈ U.

Русский

При непустом Y и клиповом множестве U равенство charFn Y hU x = 1 происходит тогда, когда x ∈ U.

LaTeX

$$charFn Y hU x = 1 ⇔ x ∈ U$$

Lean4

theorem charFn_eq_one [Nontrivial Y] (x : X) (hU : IsClopen U) : charFn Y hU x = (1 : Y) ↔ x ∈ U :=
  Set.indicator_eq_one_iff_mem _

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

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

Разделы

Аффилиация

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