subset_interior_smul_right

Mathlib.Topology.Algebra.ConstMulAction

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

← MathLib Explorer

English

s · interior(t) ⊆ interior(s · t).

Русский

s · interior(t) ⊆ interior(s · t).

LaTeX

$$$s \cdot \operatorname{int}(t) \subseteq \operatorname{int}(s \cdot t)$$$

Lean4

@[to_additive]
theorem subset_interior_smul_right {s : Set G} {t : Set α} : s • interior t ⊆ interior (s • t) :=
  interior_maximal (Set.smul_subset_smul_left interior_subset) isOpen_interior.smul_left

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

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

Разделы

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

Аффилиация

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