coborderRange

Mathlib.AlgebraicGeometry.Morphisms.Immersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Hom.coborderRange

Lean4

/-- Given an immersion `f : X ⟶ Y`, this is the biggest open set `U ⊆ Y` containing the image of `X`
such that `X` is closed in `U`.
-/
def coborderRange (f : X.Hom Y) [IsImmersion f] : Y.Opens :=
  ⟨coborder (Set.range f.base), f.isLocallyClosed_range.isOpen_coborder⟩

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

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

Разделы

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

Аффилиация

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