Proj

Mathlib.Topology.Category.Profinite.Nobeling.Basic

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.Proj

Lean4

/-- The projection mapping everything that satisfies `J i` to itself, and everything else to `false`
-/
def Proj : (I → Bool) → (I → Bool) := fun c i ↦ if J i then c i else false

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

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

Разделы

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

Аффилиация

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