image_top_eq_opensRange

Mathlib.AlgebraicGeometry.OpenImmersion

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

English

For an open immersion f, the top opens map to opensRange under f.

Русский

Для открытого вложения f верхнее множество открытостей отображается в opensRange через f.

LaTeX

$$$f.opensRange = \\text{top opens} \\text{ under } f$$$

Lean4

@[simp]
theorem image_top_eq_opensRange : f ''ᵁ ⊤ = f.opensRange :=
  by
  apply Opens.ext
  simp

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

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

Разделы

Аффилиация

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