subset_interior_div_right

Mathlib.Topology.Algebra.Group.Pointwise

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

← MathLib Explorer

English

Interior-based division left: interior(s) ÷ t ⊆ interior(s ÷ t).

Русский

interior(s) ÷ t ⊆ interior(s ÷ t).

LaTeX

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

Lean4

@[to_additive]
theorem subset_interior_div_right : s / interior t ⊆ interior (s / t) :=
  interior_maximal (div_subset_div_left interior_subset) isOpen_interior.div_left

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

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

Разделы

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

Аффилиация

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