Open additive maps with bounded lifts

An additive map between seminormed groups is open if every element has a preimage whose norm is bounded by a fixed multiple of its norm. Neither continuity nor completeness is required. This criterion turns norm-controlled lifts into quotient-topology comparisons.

theorem TauCeti.isOpenMap_of_exists_norm_le {E : Type u_1} {F : Type u_2} {𝓕 : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) {K : ℝ} (h : ∀ (y : F), ∃ (x : E), f x = y ∧ ‖x‖ ≤ K * ‖y‖) : IsOpenMap ⇑f

An additive map between seminormed groups with uniformly norm-bounded lifts is open.