continuous_proj — Mathlib

English

Let I be a type and J a predicate on I. The projection map Proj_J: (I → {0,1}) → (I → {0,1}) given by (Proj_J f)(i) = f(i) if J(i) holds, and 0 otherwise, is continuous.

Русский

Пусть I — множество индексов и J — предикат на I. Отображение проекции Proj_J: {0,1}^I → {0,1}^I, заданное (Proj_J f)(i) = f(i), если J(i) верно, иначе 0, непрерывно.

LaTeX

$$$$\\operatorname{Continuous}(\\mathrm{Proj}_J).$$$$

Lean4

@[simp]
theorem continuous_proj : Continuous (Proj J : (I → Bool) → (I → Bool)) :=
  by
  dsimp +unfoldPartialApp [Proj]
  apply continuous_pi
  intro i
  split
  · apply continuous_apply
  · apply continuous_const

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