openSegment_subset — Mathlib

English

In the product space E×F, the open segment from x to y is contained in the product of the open segments from x1 to y1 and x2 to y2.

Русский

В пространстве произведения E×F открытый сегмент от x до y содержится в произведении открытых сегментов x1→y1 и x2→y2.

LaTeX

$$$ openSegment_{\mathbb{k}}(x,y) \subseteq openSegment_{\mathbb{k}}(x_{1},y_{1}) \times^{\!} openSegment_{\mathbb{k}}(x_{2},y_{2}) $$$

Lean4

theorem openSegment_subset (x y : E × F) : openSegment 𝕜 x y ⊆ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2 :=
  by
  rintro z ⟨a, b, ha, hb, hab, hz⟩
  exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩

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