inv

Mathlib.Topology.Algebra.Group.Basic

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

English

If s is closed, then s^{-1} is closed.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem inv (hs : IsClosed s) : IsClosed s⁻¹ :=
  hs.preimage continuous_inv

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

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

Разделы

Аффилиация

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