piIcc01 — Mathlib

English

The product of closed intervals [0,1] indexed by a finite set ι forms a compact set with nonempty interior in ℝ^ι.

Русский

Произведение замкнутых интервалов [0,1], индексируемое конечной множеством ι, образует компактное множество с непустым interior в ℝ^ι.

LaTeX

$$$([0,1]^{\iota}) \text{ is compact and has nonempty interior in } \mathbb{R}^{\iota}$$$

Lean4

/-- The set `[0,1]^ι` as a compact set with non-empty interior. -/
def piIcc01 (ι : Type*) [Finite ι] : PositiveCompacts (ι → ℝ)
    where
  carrier := pi univ fun _ => Icc 0 1
  isCompact' := isCompact_univ_pi fun _ => isCompact_Icc
  interior_nonempty' := by
    simp only [interior_pi_set, Set.toFinite, interior_Icc, univ_pi_nonempty_iff, nonempty_Ioo, imp_true_iff,
      zero_lt_one]

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