restrict₂_def

Mathlib.Data.Set.Restrict

URI: https://scilib.ai/kg/mathlib#Set.restrict₂_def

English

The restriction map restrict₂ is given by composing the element a ∈ s with the inclusion s ↪ t.

Русский

Ограничение₂ задаётся композицией элемента s с инъекцией s ↪ t.

LaTeX

$$$restrict₂(\\text{hst}) = (f \\mapsto x \\mapsto f\\langle x.1, hst x.2\\rangle)$$$

Lean4

theorem restrict₂_def {s t : Set α} (hst : s ⊆ t) : restrict₂ (π := π) hst = fun f x ↦ f ⟨x.1, hst x.2⟩ :=
  rfl

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

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

Разделы

Аффилиация

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