pure_defined

Mathlib.Data.PFun

URI: https://scilib.ai/kg/mathlib#PFun.pure_defined

English

For any p ⊆ α, p ⊆ Dom of PFun.pure x for any x.

Русский

Для любого p ⊆ α выполняется p ⊆ Dom (PFun.pure x) для любого x.

LaTeX

$$$\\forall p:\\mathrm{Set}\\;\\alpha,\\; p \\subseteq \\mathrm{Dom}(\\mathrm{PFun.pure}\\; x)$$$

Lean4

theorem pure_defined (p : Set α) (x : β) : p ⊆ (@PFun.pure α _ x).Dom :=
  p.subset_univ

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

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

Разделы

Аффилиация

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