isQuotientMap_fst — Mathlib

English

The product of open sets is open in the product topology if both factors are open (and if both are nonempty).

Русский

Произведение открытых множеств открыто в топологии произведения, если оба множества открыты (и оба непусты).

LaTeX

$$$$\IsOpen(s\times t) \iff (\IsOpen(s) \land \IsOpen(t)) \lor (s = \emptyset) \lor (t = \emptyset).$$$$

Lean4

theorem isQuotientMap_fst [Nonempty Y] : IsQuotientMap (Prod.fst : X × Y → X) :=
  isOpenMap_fst.isQuotientMap continuous_fst Prod.fst_surjective

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