prod — Mathlib

English

If x1 specializes to x2 and y1 specializes to y2, then the pair (x1,y1) specializes to (x2,y2).

Русский

Если x1 специализируется на x2 и y1 специализируется на y2, то пара (x1,y1) специализируется на (x2,y2).

LaTeX

$$$$ x_1 \rightsquigarrow x_2 \land y_1 \rightsquigarrow y_2 \Rightarrow (x_1,y_1) \rightsquigarrow (x_2,y_2). $$$$

Lean4

theorem prod {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ⤳ x₂) (hy : y₁ ⤳ y₂) : (x₁, y₁) ⤳ (x₂, y₂) :=
  specializes_prod.2 ⟨hx, hy⟩

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