coe_mk' — Mathlib

English

The set obtained from mk' l u equals the product of Ioc intervals across all coordinates.

Русский

Множество, полученное из mk' l u, равно произведению интервалов Ioc по всем координатам.

LaTeX

$$$(mk'\,l\,u : Set (ι \to \mathbb{R})) = \pi univ \; (fun i \to \mathrm{Ioc}(l,i)(u,i))$$$

Lean4

@[simp]
theorem coe_mk' (l u : ι → ℝ) : (mk' l u : Set (ι → ℝ)) = pi univ fun i ↦ Ioc (l i) (u i) :=
  by
  rw [mk']; split_ifs with h
  · exact coe_eq_pi _
  · rcases not_forall.mp h with ⟨i, hi⟩
    rw [coe_bot, univ_pi_eq_empty]
    exact Ioc_eq_empty hi

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