div_right

Mathlib.Topology.Algebra.Group.Pointwise

URI: https://scilib.ai/kg/mathlib#IsOpen.div_right

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem div_right (hs : IsOpen s) : IsOpen (s / t) :=
  by
  rw [← iUnion_div_right_image]
  exact isOpen_biUnion fun a _ => isOpenMap_div_right a s hs

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

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

Разделы

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

Аффилиация

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