SwapTrue

Mathlib.Topology.Category.Profinite.Nobeling.Successor

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

English

Continuity of CC'₀.

Русский

Непрерывность CC'₀.

LaTeX

$$Continuous (CC'₀ C ho)$$

Lean4

/-- Swapping the `o`-th coordinate to `true`. -/
noncomputable def SwapTrue : (I → Bool) → I → Bool := fun f i ↦ if ord I i = o then true else f i

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

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

Разделы

Аффилиация

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