coe_coe — Mathlib

English

Let I be a box in the product space ℝ^ι. The set represented by I, when viewed as a subset of ι → ℝ, is exactly I.

Русский

Пусть I — коробка в произведении ℝ по индексу ι. Множество, соответствующее I как подмножество функций ι → ℝ, совпадает с самой коробкой I.

LaTeX

$$$((I : WithBot (Box ι)) : Set (ι \to \mathbb{R})) = I$$$

Lean4

@[simp, norm_cast]
theorem coe_coe : ((I : WithBot (Box ι)) : Set (ι → ℝ)) = I :=
  rfl

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