subtypeRestr_coe

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.subtypeRestr_coe

English

Repetition of subtypeRestr_def establishing the same relation as above.

Русский

Повторение определения subtypeRestr, устанавливающее ту же связь, что и выше.

LaTeX

$$$ e.subtypeRestr hs = (s.openPartialHomeomorphSubtypeCoe hs).trans e $$$

Lean4

@[simp, mfld_simps]
theorem subtypeRestr_coe : ((e.subtypeRestr hs : OpenPartialHomeomorph s Y) : s → Y) = Set.restrict ↑s (e : X → Y) :=
  rfl

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

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

Разделы

Аффилиация

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