instBoundedGENhdsClass — Mathlib

English

If α and β have BoundGENhdsClass, then their product α × β also has BoundGENhdsClass.

Русский

Если пространства α и β имеют BoundGENhdsClass, то их произведение α × β тоже имеет BoundGENhdsClass.

LaTeX

$$$ [BoundedGENhdsClass α] [BoundedGENhdsClass β] \Rightarrow BoundedGENhdsClass (α \times β). $$$

Lean4

instance instBoundedGENhdsClass : BoundedGENhdsClass (α × β) :=
  ⟨(Prod.instBoundedLENhdsClass (α := αᵒᵈ) (β := βᵒᵈ)).isBounded_le_nhds⟩

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