isTopologicalBasis_basic_opens — Mathlib

English

Reiterates that basicOpen(r) is open for any r.

Русский

Повторяет, что basicOpen(r) открыто для любого r.

LaTeX

$$$$ \\text{IsOpen}(\\mathrm{basicOpen}(r)). $$$$

Lean4

theorem isTopologicalBasis_basic_opens :
    TopologicalSpace.IsTopologicalBasis (Set.range fun r : R => (basicOpen r : Set (PrimeSpectrum R))) :=
  by
  apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
  · rintro _ ⟨r, rfl⟩
    exact isOpen_basicOpen
  · rintro p U hp ⟨s, hs⟩
    rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp
    obtain ⟨f, hfs, hfp⟩ := hp
    refine ⟨basicOpen f, ⟨f, rfl⟩, hfp, ?_⟩
    rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]
    exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr hfs)

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