closure_preimage_le

Mathlib.Algebra.Ring.Subring.Basic

URI: https://scilib.ai/kg/mathlib#Subring.closure_preimage_le

← MathLib Explorer

English

The range of the subtype map equals the subring: range(s.subtype) = s.

Русский

Образ отображения подпроекции равен самому подкольцу: range(s.subtype) = s.

LaTeX

$$$ \\mathrm{range}(s.\\mathrm{subtype}) = s $$$

Lean4

theorem closure_preimage_le (f : R →+* S) (s : Set S) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
  closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

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

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

Разделы

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

Аффилиация

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