English
If every x has a local section g with continuous at f x and g(f x) = x and g is a right inverse of f, then f is open.
Русский
Если для каждого x существует локальное разложение g: Y→X с непрерывностью в f(x), удовлетворяющее g(f(x)) = x и g является правым обратным к f, то f открыто.
LaTeX
$$$$\\big( \\forall x, \\Exists g: Y \\to X, \\big(\\text{ContinuousAt } g (f(x)) \\land g(f(x)) = x \\land RightInverse\, g\, f\\big) \\big) \\rightarrow IsOpenMap(f)$$$$
Lean4
theorem of_sections (h : ∀ x, ∃ g : Y → X, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f) : IsOpenMap f :=
of_nhds_le fun x =>
let ⟨g, hgc, hgx, hgf⟩ := h x
calc
𝓝 (f x) = map f (map g (𝓝 (f x))) := by rw [map_map, hgf.comp_eq_id, map_id]
_ ≤ map f (𝓝 (g (f x))) := (map_mono hgc)
_ = map f (𝓝 x) := by rw [hgx]
