restrict₂_comp_restrict

Mathlib.Data.Set.Restrict

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

English

Restrict₂ composed with t.restrict equals s.restrict when s ⊆ t.

Русский

Композиция restrict₂ с t.restrict равна restrict₂ для s, если s ⊆ t.

LaTeX

$$$\\bigl(restrict₂ (π := π) \\; hst\\bigr) \\circ t.restrict = s.restrict$$$

Lean4

theorem restrict₂_comp_restrict {s t : Set α} (hst : s ⊆ t) : (restrict₂ (π := π) hst) ∘ t.restrict = s.restrict :=
  rfl

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

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

Разделы

Аффилиация

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