instCompactIccSpaceForall — Mathlib

English

If every α_i has compactIccSpace, then the product space ∀ i, α_i has CompactIccSpace.

Русский

Если для каждого i пространство α_i имеет CompactIccSpace, то произведение пространств ∀ i, α_i также имеет CompactIccSpace.

LaTeX

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

Lean4

instance {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)] [∀ i, CompactIccSpace (α i)] :
    CompactIccSpace (∀ i, α i) :=
  ⟨fun {a b} => (pi_univ_Icc a b ▸ isCompact_univ_pi) fun _ => isCompact_Icc⟩

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