interior_smul₀

Mathlib.Topology.Algebra.ConstMulAction

URI: https://scilib.ai/kg/mathlib#interior_smul₀

← MathLib Explorer

English

For c ≠ 0, interior(c · s) = c · interior(s).

Русский

Для c ≠ 0 interior(c · s) = c · interior(s).

LaTeX

$$$\operatorname{int}(c \cdot s) = c \cdot \operatorname{int}(s)$$$

Lean4

theorem interior_smul₀ {c : G₀} (hc : c ≠ 0) (s : Set α) : interior (c • s) = c • interior s :=
  ((Homeomorph.smulOfNeZero c hc).image_interior s).symm

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

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

Разделы

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

Аффилиация

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