specializes_prod — Mathlib

English

The specialization between two pairs equals the pair of specializations: (x1,y1) ⤳ (x2,y2) iff x1 ⤳ x2 and y1 ⤳ y2.

Русский

Специализация пары равна паре специализаций: (x1,y1) ⤳ (x2,y2) эквивалентно x1 ⤳ x2 и y1 ⤳ y2.

LaTeX

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

Lean4

@[simp]
theorem specializes_prod {x₁ x₂ : X} {y₁ y₂ : Y} : (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂ := by
  simp only [Specializes, nhds_prod_eq, prod_le_prod]

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