subset_interior_div

Mathlib.Topology.Algebra.Group.Pointwise

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

← MathLib Explorer

English

Interior(s) multiplied by t is contained in interior(s·t).

Русский

Interior(s) умноженное на t содержится в interior(s·t).

LaTeX

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

Lean4

@[to_additive]
theorem subset_interior_div : interior s / interior t ⊆ interior (s / t) :=
  (div_subset_div_left interior_subset).trans subset_interior_div_left

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

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

Разделы

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

Аффилиация

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