instMin

Mathlib.Topology.Algebra.Group.GroupTopology

URI: https://scilib.ai/kg/mathlib#GroupTopology.instMin

English

The inversion map is continuous.

Русский

Обратное отображение непрерывно.

LaTeX

$$$\\mathrm{ContinuousInv}(\\mathrm{Inv.inv})$$$

Lean4

@[to_additive]
instance : Min (GroupTopology α) where min x y := ⟨x.1 ⊓ y.1, topologicalGroup_inf x.2 y.2⟩

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

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

Разделы

Аффилиация

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