subset_interior_mul

Mathlib.Topology.Algebra.Group.Pointwise

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

English

The product of interiors is contained in the interior of the product.

Русский

Произведение interior s и interior t содержится в interior(s·t).

LaTeX

$$$\\operatorname{Int}(s)\\cdot \\operatorname{Int}(t) \\subseteq \\operatorname{Int}(s\\cdot t).$$$

Lean4

@[to_additive]
theorem subset_interior_mul : interior s * interior t ⊆ interior (s * t) :=
  subset_interior_smul

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

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

Разделы

Аффилиация

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