refl_restr_source

Mathlib.Logic.Equiv.PartialEquiv

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

English

The identity equivalence restricted to a set s has source s.

Русский

Идентичность, ограниченная до множества s, имеет источник s.

LaTeX

$$$((\\mathrm{PartialEquiv.refl} \\alpha).\\mathrm{restr}~s).\\mathrm{source} = s$$$

Lean4

@[mfld_simps]
theorem refl_restr_source (s : Set α) : ((PartialEquiv.refl α).restr s).source = s := by simp

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

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

Разделы

Аффилиация

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