toContinuousInf — Mathlib

English

The map sSupHom between complete lattices is continuous with respect to the lower topology when viewed in the dual setting.

Русский

Отображение sSupHom между полными решётками непрерывно относительно нижней топологии при двойственном отображении.

LaTeX

$$$\text{Continuous}(f)\;\text{for } f: sSupHom(\alpha,\beta)$$$

Lean4

instance (priority := 90) toContinuousInf : ContinuousSup α :=
  ⟨(supsSupHom : sSupHom (α × α) α).continuous⟩

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