instPartialOrder — Mathlib

English

The ordering on ring topologies on R is defined by refinement of open sets: t ≤ s if every s-open set is t-open.

Русский

Упорядочение топологий кольца на R задается по включению открытых множеств: t ≤ s, если каждый открытый множитель в s также открытый в t.

LaTeX

$$t ≤ s if IsOpen_s ⊆ IsOpen_t$$

Lean4

/-- The ordering on ring topologies on the ring `R`.
  `t ≤ s` if every set open in `s` is also open in `t` (`t` is finer than `s`). -/
instance : PartialOrder (RingTopology R) :=
  PartialOrder.lift RingTopology.toTopologicalSpace toTopologicalSpace_injective

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