closure_prod_eq — Mathlib

English

The second projection is a quotient map when X is nonempty.

Русский

Вторая проекция является факторным отображением при непустом X.

LaTeX

$$$$[\text{Nonempty } X] \Rightarrow \text{IsQuotientMap}(\mathrm{Prod.snd}).$$$$

Lean4

theorem closure_prod_eq {s : Set X} {t : Set Y} : closure (s ×ˢ t) = closure s ×ˢ closure t :=
  ext fun ⟨a, b⟩ => by simp_rw [mem_prod, mem_closure_iff_nhdsWithin_neBot, nhdsWithin_prod_eq, prod_neBot]

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