prod — Mathlib

English

If s₁ ⊆ X and s₂ ⊆ Y are closed, then s₁ ×ˢ s₂ is closed in X × Y.

Русский

Если s₁ ⊆ X и s₂ ⊆ Y замкнуты, то s₁ ×ˢ s₂ замкнуто в X×Y.

LaTeX

$$$$\mathrm{IsClosed}(s_1) \land \mathrm{IsClosed}(s_2) \Rightarrow \mathrm{IsClosed}(s_1 \times\!s_2).$$$$

Lean4

theorem prod {s₁ : Set X} {s₂ : Set Y} (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) : IsClosed (s₁ ×ˢ s₂) :=
  closure_eq_iff_isClosed.mp <| by simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]

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