Structures · Topology

ContinuousSup

Let L be a topological space and let L×L be equipped with the product topology and let ⊓:L×L → L be a supremum. Then L is said to have (jointly) continuous supremum if the map ⊓:L×L → L is continuous.

Defined in

Mathlib.Topology.Order.Lattice

Shape

One type argument · adds continuous_sup