instBoundedLENhdsClass — Mathlib

English

The product α × β carries a canonical bounded LENhdsClass structure, obtained from α and β.

Русский

Произведение α × β обладает канонической структурой boundedLENhdsClass, получаемой из α и β.

LaTeX

$$$$ \text{BoundedLENhdsClass }(\alpha \times \beta). $$$$

Lean4

instance instBoundedLENhdsClass : BoundedLENhdsClass (α × β) :=
  by
  refine ⟨fun x ↦ ?_⟩
  obtain ⟨a, ha⟩ := isBounded_le_nhds x.1
  obtain ⟨b, hb⟩ := isBounded_le_nhds x.2
  rw [← @Prod.mk.eta _ _ x, nhds_prod_eq]
  exact ⟨(a, b), ha.prod_mk hb⟩

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