instPartialOrder — Mathlib

English

Topologies on a set α are ordered by refinement: t is finer than s if every open set of s is open in t.

Русский

Топологии на множествах α упорядочиваются по уточнению: t тоньше, чем s, если каждая открытая множество из s также открыта в t.

LaTeX

$$$t \\le s \\iff \\forall U, \\IsOpen[s](U) \\rightarrow \\IsOpen[t](U)$$$

Lean4

/-- The ordering on topologies on the type `α`. `t ≤ s` if every set open in `s` is also open in `t`
(`t` is finer than `s`). -/
instance : PartialOrder (TopologicalSpace α) :=
  { PartialOrder.lift (fun t => OrderDual.toDual IsOpen[t]) (fun _ _ => TopologicalSpace.ext) with
    le := fun s t => ∀ U, IsOpen[t] U → IsOpen[s] U }

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