one

Mathlib.Topology.Algebra.Support

URI: https://scilib.ai/kg/mathlib#HasCompactMulSupport.one

← MathLib Explorer

English

The constant function 1 has compact multiplicative support.

Русский

Постоянная функция 1 имеет компактную мультиподдержку.

LaTeX

$$$\\text{HasCompactMulSupport}(1: \\alpha\\to \\beta).$$$

Lean4

@[to_additive, simp]
protected theorem one {α β : Type*} [TopologicalSpace α] [One β] : HasCompactMulSupport (1 : α → β) := by
  simp [HasCompactMulSupport, mulTSupport]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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