continuous — Mathlib

English

Any infimum-homomorphism between complete lattices is a continuous map in the lower topology.

Русский

Любое отображение-сохраняющее наименьшее (infimum) между полными решётками непрерывно в нижней топологии.

LaTeX

$$$\text{Continuous}(f)\quad\text{for }f: sInfHom(\alpha,\beta)$$$

Lean4

protected theorem _root_.sInfHom.continuous (f : sInfHom α β) : Continuous f :=
  by
  refine IsLower.continuous_iff_Ici.2 fun b => ?_
  convert isClosed_Ici (a := sInf <| f ⁻¹' Ici b)
  refine Subset.antisymm (fun a => sInf_le) fun a ha => le_trans ?_ <| OrderHomClass.mono (f : α →o β) ha
  refine LE.le.trans ?_ (map_sInf f _).ge
  simp
    -- see Note [lower instance priority]

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