charFn_inj

Mathlib.Topology.LocallyConstant.Algebra

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

← MathLib Explorer

English

If two clopen sets U and V have equal charFn functions, then U = V.

Русский

Если две клиповские множества U и V имеют одинаковые функции-индикаторы, то U = V.

LaTeX

$$charFn Y hU = charFn Y hV → U = V$$

Lean4

theorem charFn_inj [Nontrivial Y] (hU : IsClopen U) (hV : IsClopen V) (h : charFn Y hU = charFn Y hV) : U = V :=
  Set.indicator_one_inj Y <| coe_inj.mpr h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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