instBoundedSpaceForall — Mathlib

English

If α and β are bounded spaces, then the product α × β is a bounded space.

Русский

Если пространства α и β ограничены, то их произведение α × β ограничено.

LaTeX

$$$[\\text{BoundedSpace } \\alpha] \\land [\\text{BoundedSpace } \\beta] \\Rightarrow \\text{BoundedSpace}(\\alpha \\times \\beta)$$$

Lean4

instance [∀ i, BoundedSpace (X i)] : BoundedSpace (∀ i, X i) := by simp [← cobounded_eq_bot_iff, cobounded_pi]

Похожие утверждения