mem_restrict

Mathlib.Data.PFun

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

English

If s ⊆ f.Dom, then b ∈ f.restrict h a iff a ∈ s ∧ b ∈ f a.

Русский

Пусть s ⊆ Dom f; тогда b ∈ f.restrict h a тогда и только тогда, когда a ∈ s и b ∈ f(a).

LaTeX

$$$b \\in f|_{h}(a) \\iff a \\in s \\wedge b \\in f(a)$$$

Lean4

@[simp]
theorem mem_restrict {f : α →. β} {s : Set α} (h : s ⊆ f.Dom) (a : α) (b : β) : b ∈ f.restrict h a ↔ a ∈ s ∧ b ∈ f a :=
  by simp [restrict]

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

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

Разделы

Аффилиация

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