restr_univ

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#PartialEquiv.restr_univ

English

Restricting e to the universal set leaves e unchanged: e|_{univ} = e.

Русский

Ограничение e до всеобъемлющего множества не изменяет e: e|_{univ} = e.

LaTeX

$$$e|_{\mathrm{univ}} = e$$$

Lean4

@[simp, mfld_simps]
theorem restr_univ {e : PartialEquiv α β} : e.restr univ = e :=
  restr_eq_of_source_subset (subset_univ _)

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

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

Разделы

Аффилиация

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