continuous_div_left' — Mathlib

English

For a fixed a ∈ G, the map x ↦ a / x is continuous in a topological group G with continuous division.

Русский

Для фиксированного a ∈ G отображение x ↦ a / x непрерывно в топологической группе G с непрерывным делением.

LaTeX

$$$\text{Continuous}(\lambda x. a / x).$$$

Lean4

@[to_additive (attr := continuity) continuous_sub_left]
theorem continuous_div_left' (a : G) : Continuous (a / ·) :=
  continuous_const.div' continuous_id

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