preimage_subset_dom

Mathlib.Data.PFun

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

English

The preimage of any set under f is contained in the domain of f.

Русский

Предобраз любого множества под f содержится в области определения f.

LaTeX

$$$f.preimage s \\subseteq f.Dom$$$

Lean4

theorem preimage_subset_dom (s : Set β) : f.preimage s ⊆ f.Dom := fun _ ⟨y, _, fxy⟩ => Part.dom_iff_mem.mpr ⟨y, fxy⟩

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

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

Разделы

Аффилиация

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