basicOpen_eq_bot_iff — Mathlib

English

basicOpen f equals bottom if and only if f is nilpotent.

Русский

basicOpen(f) равно нулю тогда и только тогда, когда f nilpotent.

LaTeX

$$$$ \\mathrm{basicOpen}(f) = \\bot \\iff \\mathrm{IsNilpotent}(f). $$$$

Lean4

@[simp]
theorem basicOpen_eq_bot_iff (f : R) : basicOpen f = ⊥ ↔ IsNilpotent f :=
  by
  rw [← TopologicalSpace.Opens.coe_inj, basicOpen_eq_zeroLocus_compl]
  simp only [Set.eq_univ_iff_forall, Set.singleton_subset_iff, TopologicalSpace.Opens.coe_bot, nilpotent_iff_mem_prime,
    Set.compl_empty_iff, mem_zeroLocus, SetLike.mem_coe]
  exact ⟨fun h I hI => h ⟨I, hI⟩, fun h ⟨I, hI⟩ => h I hI⟩

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