isOpen_prod_iff — Mathlib

English

A product set s × t is open in X × Y iff either s and t are open, or one of s,t is empty.

Русский

Произведение открыто в X × Y тогда, когда либо s и t открыты, либо одно из них пусто.

LaTeX

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

Lean4

theorem isOpen_prod_iff {s : Set (X × Y)} :
    IsOpen s ↔ ∀ a b, (a, b) ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s :=
  isOpen_iff_mem_nhds.trans <| by simp_rw [Prod.forall, mem_nhds_prod_iff', and_left_comm]

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