sketch why Ban has cartesian filtered colimits

Author: ScriptRaccoon

database/data/004_property-assignments/Ban.sql

@@ -23,6 +23,12 @@ VALUES
 	TRUE,
 	'Example 1.48 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>.'
 ),
+(
+	'Ban',
+	'cartesian filtered colimits',
+	TRUE,
+	'If $X$ is a Banach space and $(Y_i)$ is a filtered diagram of Banach spaces, the canonical map $\mathrm{colim}_i (X \times Y_i) \to X \times \mathrm{colim}_i Y_i$ is the completion of the canonical map in the category of normed vector spaces with non-expansive linear maps. Now the claim follows directly from the <a href="/category/Met">category of metric spaces</a> with non-expansive maps.'
+),
 (
 	'Ban',
 	'cogenerator',