eval_image_pi_subset

Mathlib.Data.Set.Prod

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

English

If i ∈ s, then eval i applied to s.pi t is contained in t i.

Русский

Если i ∈ s, то образ eval_i от s.pi t содержится в t_i.

LaTeX

$$$ \operatorname{eval}_i''(s.\pi t) \subseteq t_i $$$

Lean4

theorem eval_image_pi_subset (hs : i ∈ s) : eval i '' s.pi t ⊆ t i :=
  image_subset_iff.2 fun _ hf => hf i hs

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

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

Разделы

Аффилиация

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