instInv

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.instInv

English

If there is an Inv structure on G, then Germ_l G inherits Inv by applying the inverse inside the germ map.

Русский

Если на G задана структура Inv, то Germ_l G наследует инверсию через отображение жерма.

LaTeX

$$$[Inv\\ G] \\Rightarrow Inv(\\mathrm{Germ}_l G).$$$

Lean4

@[to_additive]
instance instInv [Inv G] : Inv (Germ l G) :=
  ⟨map Inv.inv⟩

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

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

Разделы

Аффилиация

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