preimage_eq_top_of_closedPoint_mem

English

If the image of the closed point under f lies in an open U, then the preimage of U under f is the whole domain.

Русский

Если образ замкнутой точки под f лежит в открытом U, то предобраз U под f равен всему множеству.

LaTeX

$$$f.base(\\mathrm{closedPoint}\\ R) \\in U \\implies f^{-1}\\!\\_U U = \\top$$$

Lean4

theorem preimage_eq_top_of_closedPoint_mem {U : Opens X} (hU : f.base (closedPoint R) ∈ U) : f ⁻¹ᵁ U = ⊤ :=
  IsLocalRing.closed_point_mem_iff.mp hU

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