English
Characterizes openness of product sets in terms of openness of factors or emptiness.
Русский
Характеризует открытость произведений множеств через открытость факторов или пустоту.
LaTeX
$$$$\text{IsOpen}(s\times s') \iff (\text{IsOpen}(s) \land \text{IsOpen}(s')) \lor s = \emptyset \lor s' = \emptyset.$$$$
Lean4
/-- A product set is open in a product space if and only if each factor is open, or one of them is
empty -/
theorem isOpen_prod_iff' {s : Set X} {t : Set Y} : IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅ :=
by
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
· simp [h, prod_eq_empty_iff.1 h]
· have st : s.Nonempty ∧ t.Nonempty := prod_nonempty_iff.1 h
constructor
· intro (H : IsOpen (s ×ˢ t))
refine Or.inl ⟨?_, ?_⟩
· simpa only [fst_image_prod _ st.2] using isOpenMap_fst _ H
· simpa only [snd_image_prod st.1 t] using isOpenMap_snd _ H
· intro H
simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
exact H.1.prod H.2
