inv

Mathlib.Topology.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#IsCompact.inv

English

If s ⊆ G is compact, then s^{-1} is compact.

Русский

Если множество s в G компактно, то s^{-1} тоже компактно.

LaTeX

$$$IsCompact\\ s \\Rightarrow IsCompact\\ s^{-1}.$$$

Lean4

@[to_additive]
theorem inv (hs : IsCompact s) : IsCompact s⁻¹ :=
  by
  rw [← image_inv_eq_inv]
  exact hs.image continuous_inv

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru