Module

PrimeSpectrum_apply_eq_apply_of_forall_le_of_connectedSpace.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.PrimeSpectrum_apply_eq_apply_of_forall_le_of_connectedSpace

1 declaration indexed from sourceView source ↗

Module documentation

Prime Spectrum apply eq apply of forall le of connected Space

Imports2

Mathlib.RingTheory.Spectrum.Prime.Noetherian
Mathlib.Tactic.Ext

Imported by2

theorem

apply_eq_apply_of_forall_le_of_connectedSpace

L27 ↗

PrimeSpectrum.apply_eq_apply_of_forall_le_of_connectedSpace

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace PrimeSpectrum_apply_eq_apply_of_forall_le_of_connectedSpace
universe u v

Lean source · statement

theorem _root_.PrimeSpectrum.apply_eq_apply_of_forall_le_of_connectedSpace
    {R : Type u} [CommRing R] [IsNoetherianRing R] [ConnectedSpace (PrimeSpectrum R)]
    {α : Type v} (φ : PrimeSpectrum R → α)
    (h : ∀ p q : PrimeSpectrum R, p ≤ q → φ p = φ q) (p q : PrimeSpectrum R) :
    φ p = φ q

Module documentation

Prime Spectrum apply eq apply of forall le of connected Space

Declarations

apply_eq_apply_of_forall_le_of_connectedSpace