continuous_projRestrict — Mathlib

English

Let C be a set of functions I → Bool and J an I → Prop. The restricted projection ProjRestrict C J is continuous.

Русский

Пусть C — множество функций I → Bool, и J — отображение I → пропозиция. Ограниченная проекция ProjRestrict C J непрерывна.

LaTeX

$$$$\\operatorname{Continuous}(\\mathrm{ProjRestrict}\\, C\\, J).$$$$

Lean4

@[simp]
theorem continuous_projRestrict : Continuous (ProjRestrict C J) :=
  Continuous.restrict _ (continuous_proj _)

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