ofSet_target

Mathlib.Logic.Equiv.PartialEquiv

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

English

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

Русский

Цель идентичной частичной эквивалентности на s равна s.

LaTeX

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

Lean4

@[simp, mfld_simps]
theorem ofSet_target (s : Set α) : (PartialEquiv.ofSet s).target = s :=
  rfl

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

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

Разделы

Аффилиация

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