fundamentalDomain_pi_basisFun — Mathlib

English

For a finite index set ι, the fundamental domain of the real Pi-basis equals the product of intervals [0,1) over all i in ι.

Русский

Для конечного множества индексов ι фундаментальная область Pi-базиса на реальном числе равна произведению отрезков [0,1) по всем i∈ι.

LaTeX

$$$ \operatorname{fundamentalDomain}(\Pi\text{basisFun }\mathbb{R}, ι) = \mathrm{Set.univ} \pi \!\, (\lambda i: \mathrm{Set.Ico}(0,1)) $$$

Lean4

theorem fundamentalDomain_pi_basisFun [Fintype ι] :
    fundamentalDomain (Pi.basisFun ℝ ι) = Set.pi Set.univ fun _ : ι ↦ Set.Ico (0 : ℝ) 1 := by ext; simp

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