eval_image_univ_pi

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.eval_image_univ_pi

English

The image of Pi.map f on s.pi t is contained in s.pi of f i image t i.

Русский

Образ Pi.map f на s.pi t содержится в s.pi (f i) образ t i.

LaTeX

$$$ \Pi.map f '' s.pi t \subseteq s.pi (\lambda i. f i '' t i)$$$

Lean4

@[simp]
theorem eval_image_univ_pi (ht : (pi univ t).Nonempty) : (fun f : ∀ i, α i => f i) '' pi univ t = t i :=
  eval_image_pi (mem_univ i) ht

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

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

Разделы

Аффилиация

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