openPartialHomeomorphSubtypeCoe_target

English

The target of s.openPartialHomeomorphSubtypeCoe hs is the open set s.

Русский

Цель отображения s.openPartialHomeomorphSubtypeCoe hs равна открытой множеству s.

LaTeX

$$$ (s.openPartialHomeomorphSubtypeCoe hs).target = s $$$

Lean4

@[simp, mfld_simps]
theorem openPartialHomeomorphSubtypeCoe_target : (s.openPartialHomeomorphSubtypeCoe hs).target = s :=
  by
  simp only [openPartialHomeomorphSubtypeCoe, Subtype.range_coe_subtype, mfld_simps]
  rfl

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