isOpen_of_isOpen_subideal

Mathlib.Topology.Algebra.OpenSubgroup

URI: https://scilib.ai/kg/mathlib#Ideal.isOpen_of_isOpen_subideal

← MathLib Explorer

English

If U ≤ P are submodules and U is open, then P is open as well.

Русский

Если U является подмодулем внутри P и U открыто, то P тоже открыто.

LaTeX

$$$U \\le P$ and $U\\text{ isOpen} \\Rightarrow P\\text{ isOpen}$$$

Lean4

theorem isOpen_of_isOpen_subideal {U I : Ideal R} (h : U ≤ I) (hU : IsOpen (U : Set R)) : IsOpen (I : Set R) :=
  @Submodule.isOpen_mono R R _ _ _ _ Semiring.toModule _ _ h hU

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

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

Разделы

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

Аффилиация

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