isOpen_range — Mathlib

English

For an open immersion f, the underlying topological range of f is open.

Русский

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

LaTeX

$$$\\text{If } f:\\,X\\to Y\\text{ is an open immersion, then }\\mathrm{range}(f\\!\\text{base})\\text{ is open.}$$$

Lean4

theorem isOpen_range {X Y : Scheme.{u}} (f : X ⟶ Y) [H : IsOpenImmersion f] : IsOpen (Set.range f.base) :=
  H.base_open.isOpen_range

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