Prod

📁 Source: Mathlib/Order/ScottContinuity/Prod.lean

Statistics

Metric	Count
Definitions	0
Theorems fromProd, prod, fromProd	3
Total	3

ScottContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromProd 📖	mathematical	ScottContinuous	Prod.instPreorder	—	ScottContinuousOn.fromProd scottContinuousOn monotone
prod 📖	mathematical	ScottContinuous	Prod.instPreorder	—	fromProd Set.ext Set.image_congr IsLUB.prod Set.singleton_nonempty Set.Nonempty.image isLUB_singleton

ScottContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromProd 📖	mathematical	ScottContinuousOn Set.image Set Monotone	Prod.instPreorder	—	isLUB_congr Monotone.upperBounds_image_of_directedOn_prod monotone_prod_iff Set.iUnion_of_singleton_coe Set.iUnion_prod_const Set.image_iUnion isLUB_iUnion_iff_of_isLUB Set.singleton_prod Set.image_image Set.mem_image_of_mem Set.Nonempty.image DirectedOn.snd isLUB_prod Set.range.eq_1 Set.ext DirectedOn.fst

---

← Back to Index