continuous_div_right' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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