compact_Icc_space' — Mathlib

English

If each α_i has a CompactIccSpace, then the function space ∀ i, α_i has CompactIccSpace.

Русский

Если каждый α_i имеет CompactIccSpace, то пространство функций ∀ i, α_i имеет CompactIccSpace.

LaTeX

$$∀ {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)] [∀ i, CompactIccSpace (α i)], CompactIccSpace (∀ i, α i)$$

Lean4

instance compact_Icc_space' {α β : Type*} [Preorder β] [TopologicalSpace β] [CompactIccSpace β] :
    CompactIccSpace (α → β) :=
  inferInstance

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