Ioo — Mathlib

English

The interior of a box is the box Ioo in the sense of an order hom to subsets of coordinates.

Русский

Внутренность коробки задается как Box.Ioo в виде отображения в подмножество по координатам.

LaTeX

$$Box.Ioo : Box ι →o Set (ι → ℝ)$$

Lean4

/-- The interior of a box. -/
protected def Ioo : Box ι →o Set (ι → ℝ)
    where
  toFun I := pi univ fun i ↦ Ioo (I.lower i) (I.upper i)
  monotone' _ _ h := pi_mono fun i _ ↦ Ioo_subset_Ioo ((le_iff_bounds.1 h).1 i) ((le_iff_bounds.1 h).2 i)

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