instIsTopologicalGroup — Mathlib

English

The unit sphere S = { z ∈ 𝕜 : ∥z∥ = 1 } is a topological group under multiplication, i.e., the multiplication and inversion are continuous in the subspace topology induced from 𝕜.

Русский

Единичная сфера S = { z ∈ 𝕜 : ∥z∥ = 1 } является топологической группой относительно умножения: умножение и взятие обратной непрерывны в подпространственной топологии 𝕜.

LaTeX

$$$$\\text{IsTopologicalGroup}(\\mathrm{sphere}(0,1)),$$$$

Lean4

instance instIsTopologicalGroup [NormedDivisionRing 𝕜] : IsTopologicalGroup (sphere (0 : 𝕜) 1) where
  continuous_inv := (continuous_subtype_val.inv₀ ne_zero_of_mem_unit_sphere).subtype_mk _

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