inseparable_prod — Mathlib

English

For elements x1, x2 in X and y1, y2 in Y, the inseparability of the product (x1, y1) and (x2, y2) holds exactly when x1 and x2 are inseparable and y1 and y2 are inseparable.

Русский

Для элементов x1, x2 ∈ X и y1, y2 ∈ Y неразделимость пары (x1, y1) и (x2, y2) эквивалентна тому, что x1 и x2 неразделимы и что y1 и y2 неразделимы в своих пространствах.

LaTeX

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

Lean4

@[simp]
theorem inseparable_prod {x₁ x₂ : X} {y₁ y₂ : Y} : ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂) := by
  simp only [Inseparable, nhds_prod_eq, prod_inj]

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