inv

Mathlib.Topology.LocallyConstant.Basic

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

English

If f: X → Y is locally constant and Y has an inversion, then the map x ↦ f(x)^{-1} is locally constant.

Русский

Если f: X → Y локально константна и у Y есть обратимый элемент, то x ↦ f(x)^{-1} локально константен.

LaTeX

$$IsLocallyConstant f⁻¹$$

Lean4

@[to_additive]
theorem inv [Inv Y] ⦃f : X → Y⦄ (hf : IsLocallyConstant f) : IsLocallyConstant f⁻¹ :=
  hf.comp fun x => x⁻¹

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

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

Разделы

Аффилиация

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