English
Let f be approximated linearly on s with a linear surrogate f' and a nonlinear right inverse f'. If s is open and either F is trivial or the approximation constant c is strictly smaller than the reciprocal of the nonlinear inverse's norm, then the image f(s) is open.
Русский
Пусть f аппроксимируется линейно на nesh s с линейным приближением f' и есть нелинейное правое обратное f'. Если s открыто и либо F тривиально, либо константа приближённости c меньше обратной нормы f'symm, образ f(s) является открытым.
LaTeX
$$$\text{If } hf: \ ApproximatesLinearOn(f,f',s,c)\text{ and } f'\text{ has a nonlinear right inverse } f',\text{ with } hs: IsOpen(s)\text{ and } (Subsingleton F \lor c < (f'symm.nnnorm)^{-1}),\text{ then } IsOpen(f\,''\,s).$$$
Lean4
theorem open_image (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) (hs : IsOpen s)
(hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹) : IsOpen (f '' s) :=
by
rcases hc with hE | hc
· exact isOpen_discrete _
simp only [isOpen_iff_mem_nhds, nhds_basis_closedBall.mem_iff, forall_mem_image] at hs ⊢
intro x hx
rcases hs x hx with ⟨ε, ε0, hε⟩
refine ⟨(f'symm.nnnorm⁻¹ - c) * ε, mul_pos (sub_pos.2 hc) ε0, ?_⟩
exact (hf.surjOn_closedBall_of_nonlinearRightInverse f'symm (le_of_lt ε0) hε).mono hε Subset.rfl
