instOrderTop — Mathlib

English

There is a top element in the ordered set of ideal sheaf data, given by top. The corresponding ideal on every open is ⊤.

Русский

У упорядоченного набора данных идеалов существует наивысший элемент, заданный как верхний; соответствующий идеал на каждом открытом равен ⊤.

LaTeX

$$$\text{top} \in X.\text{IdealSheafData}$ with \text{top.ideal} = \top$$$

Lean4

instance : OrderTop (IdealSheafData X) where
  top.ideal := ⊤
  top.map_ideal_basicOpen := by simp [Ideal.map_top]
  top.supportSet := ⊥
  top.supportSet_eq_iInter_zeroLocus := by
    ext x
    simpa using (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
  le_top I U := le_top

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