Theorems · Inductive type · general topology

ContinuousSup

(L : Type u_1) → [TopologicalSpace L] → [Max L] → Prop

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

Cited by

70 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceMax