instIsUpperSet — Mathlib

English

For a given preorder α, the space α with the upper set topology is itself an upper-set space.

Русский

Для данного порядка α пространство α с топологией верхних множеств является пространством верхних множеств.

LaTeX

$$$ \,[Preorder \alpha] \Rightarrow \mathrm{Topology.IsUpperSet} (\mathrm{WithUpperSet} \alpha).$$$

Lean4

instance [Preorder α] : @Topology.IsUpperSet α (upperSet α) _ :=
  by
  letI := upperSet α
  exact ⟨rfl⟩

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