Commit 2025-10-09 17:08 16d3e097

View on Github →

feat(Order/ScottContinuity): Scott continuity on product spaces (#26338) Some further results on Scott Continuity:

  • scottContinuous_iff_map_sSup: f is Scott continuous if and only if it commutes with sSup on directed sets
  • ScottContinuous_prod_of_ScottContinuous: f is Scott continuous on a product space if it is Scott continuous in each variable
  • ScottContinuousOn.inf₂: For complete linear orders, the meet operation is Scott continuous

Estimated changes

added theorem IsGLB.prod
added theorem IsLUB.prod
added theorem lowerBounds_prod
added theorem upperBounds_prod
added theorem ScottContinuous.inf₂
added theorem ScottContinuous.prod