subset_interior_mul_right

Mathlib.Topology.Algebra.Group.Pointwise

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

English

s • interior t is contained in interior of 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_mul_right : s * interior t ⊆ interior (s * t) :=
  subset_interior_smul_right

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

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

Разделы

Аффилиация

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