instIsOrderBornology — Mathlib

English

The function space ∀ i, α_i inherits IsOrderBornology if each α_i has Preorder, Bornology, and IsOrderBornology.

Русский

Пространство функций ∀ i, α_i наследует IsOrderBornology, если каждый α_i имеет упорядочение, борологию и IsOrderBornology.

LaTeX

$$$\operatorname{IsOrderBornology}(\forall i, \alpha_i)$$$

Lean4

instance instIsOrderBornology {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, Bornology (α i)]
    [∀ i, IsOrderBornology (α i)] : IsOrderBornology (∀ i, α i) where
  isBounded_iff_bddBelow_bddAbove
    s := by
    simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and, isBounded_iff_bddBelow_bddAbove]

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