toOpenPartialHomeomorph_source — Mathlib

English

The source of the open partial homeomorph is exactly s.

Русский

Источником открытого частичного гомоморфа является ровно множество s.

LaTeX

$$$( hf.toOpenPartialHomeomorph f s hc hs ).source = s$$$

Lean4

@[simp]
theorem toOpenPartialHomeomorph_source (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
    (hc : Subsingleton E ∨ c < N⁻¹) (hs : IsOpen s) : (hf.toOpenPartialHomeomorph f s hc hs).source = s :=
  rfl

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