subtypeRestr_def — Mathlib

English

The subtype-restricted map e.subtypeRestr hs is defined as the transitive composition of the subtype embedding with e.

Русский

Ограничение по подтипу через подтиповую вставку определяется как композиция подтипового вложения с e.

LaTeX

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

Lean4

theorem subtypeRestr_def : e.subtypeRestr hs = (s.openPartialHomeomorphSubtypeCoe hs).trans e :=
  rfl

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