div_left

Mathlib.Topology.Algebra.Group.Pointwise

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

← MathLib Explorer

English

Interior-based division left inequality: interior(s) ÷ t is contained in interior(s ÷ t).

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem div_left (ht : IsOpen t) : IsOpen (s / t) :=
  by
  rw [← iUnion_div_left_image]
  exact isOpen_biUnion fun a _ => isOpenMap_div_left a t ht

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

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

Разделы

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

Аффилиация

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