coe_charFn

Mathlib.Topology.LocallyConstant.Algebra

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

English

The underlying function of charFn is exactly the set-theoretic indicator of U with value 1.

Русский

Основная функция charFn равна индикатору множества U со значением 1.

LaTeX

$$(charFn Y hU : X → Y) = Set.indicator U 1$$

Lean4

theorem coe_charFn (hU : IsClopen U) : (charFn Y hU : X → Y) = Set.indicator U 1 :=
  rfl

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

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

Разделы

Аффилиация

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