interior_smul

Mathlib.Topology.Algebra.ConstMulAction

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

English

The interior of c · s equals c · interior(s) for any fixed c ∈ G.

Русский

interior( c · s ) = c · interior(s).

LaTeX

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

Lean4

@[to_additive]
theorem interior_smul (c : G) (s : Set α) : interior (c • s) = c • interior s :=
  ((Homeomorph.smul c).image_interior s).symm

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

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

Разделы

Аффилиация

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