isOpenMap_of_ne_zero — Mathlib

English

A nonzero continuous linear functional is an open map; the open mapping is constructed via a local open sections argument.

Русский

Непрерывный линейный функционал, не ноль, является открытым отображением; открытость достигается через секции локальных открытых множеств.

LaTeX

$$IsOpenMap f$$

Lean4

/-- A nonzero continuous linear functional is open. -/
protected theorem isOpenMap_of_ne_zero [TopologicalSpace R] [DivisionRing R] [ContinuousSub R] [AddCommGroup M]
    [TopologicalSpace M] [ContinuousAdd M] [Module R M] [ContinuousSMul R M] (f : StrongDual R M) (hf : f ≠ 0) :
    IsOpenMap f :=
  let ⟨x, hx⟩ := exists_ne_zero hf
  IsOpenMap.of_sections fun y =>
    ⟨fun a => y + (a - f y) • (f x)⁻¹ • x, Continuous.continuousAt <| by fun_prop, by simp, fun a => by simp [hx]⟩

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