isIdempotentElemEquivClopens_symm_bot

Mathlib.RingTheory.Spectrum.Prime.Topology

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot

English

The idempotent corresponding to the bottom clopen (the empty set) is the zero element 0 of the ring.

Русский

Идемпотент, соответствующий нижнему клозоподмножеству (пустое множество), равен нулю кольца.

LaTeX

$$e^{−1}(\bot) = ⟨0, ·\;\rbrace⟩$$

Lean4

theorem isIdempotentElemEquivClopens_symm_bot : isIdempotentElemEquivClopens.symm ⊥ = ⟨(0 : R), .zero⟩ :=
  map_bot _

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

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

Разделы

Аффилиация

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