refl_target

Mathlib.Logic.Equiv.PartialEquiv

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

English

The source of the identity partial equivalence on a set s is s.

Русский

Область определения идентичной частичной эквивалентности на s равна s.

LaTeX

$$$\operatorname{source}(\mathrm{ofSet}(s)) = s$$$

Lean4

@[simp, mfld_simps]
theorem refl_target : (PartialEquiv.refl α).target = univ :=
  rfl

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

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

Разделы

Аффилиация

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