dom_toSubtype

Mathlib.Data.PFun

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

English

The domain of the toSubtype construction with a predicate p matches the set {a | p(f(a))}.

Русский

Область определения конструкции toSubtype совпадает с множеством {a | p(f(a))}.

LaTeX

$$$$ (toSubtype(p,f)).Dom = \{ a \mid p(f(a)) \}. $$$$

Lean4

@[simp]
theorem dom_toSubtype (p : β → Prop) (f : α → β) : (toSubtype p f).Dom = {a | p (f a)} :=
  rfl

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

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

Разделы

Аффилиация

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