toOpenPartialHomeomorph_target — Mathlib

English

The target of the open partial homeomorph is f''s.

Русский

Целевой образ открытого частичного гомоморфа равен образу f'' s.

LaTeX

$$$( hf.toOpenPartialHomeomorph f s hc hs ).target = f '' s$$$

Lean4

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

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