openSegment_subset — Mathlib

English

Analogous statement for open segments: the open segment between x and y lies inside the product of open segments in each coordinate.

Русский

Аналогично для открытого сегмента: открытый сегмент между x и y лежит внутри произведения открытых сегментов по каждой координате.

LaTeX

$$$$\operatorname{openSegment}_{\mathbb{k}}(x,y) \subseteq s\,\pi\,\lambda i.\operatorname{openSegment}_{\mathbb{k}}(x_i,y_i).$$$$

Lean4

theorem openSegment_subset (x y : ∀ i, M i) : openSegment 𝕜 x y ⊆ s.pi fun i => openSegment 𝕜 (x i) (y i) :=
  by
  rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
  exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩

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