openPartialHomeomorphSubtypeCoe_source

English

The source of the map s.openPartialHomeomorphSubtypeCoe hs is the universal set, i.e., the source is Set.univ.

Русский

Источник отображения s.openPartialHomeomorphSubtypeCoe hs равен все множеству, то есть источник — Set.univ.

LaTeX

$$$ (s.openPartialHomeomorphSubtypeCoe hs).source = \mathrm{Set.univ} $$$

Lean4

@[simp, mfld_simps]
theorem openPartialHomeomorphSubtypeCoe_source : (s.openPartialHomeomorphSubtypeCoe hs).source = Set.univ :=
  rfl

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