prod_eq_univ — Mathlib

English

If α and β are nonempty, then s × t = univ if and only if s = univ and t = univ.

Русский

Если множества α и β непусты, то s × t = univ тогда и только тогда, когда s = univ и t = univ.

LaTeX

$$$ [\text{Nonempty } \alpha] [\text{Nonempty } \beta] : (s \times t = \mathrm{univ}) \iff (s = \mathrm{univ} \wedge t = \mathrm{univ}) $$$

Lean4

@[simp]
theorem prod_eq_univ [Nonempty α] [Nonempty β] : s ×ˢ t = univ ↔ s = univ ∧ t = univ := by
  simp [eq_univ_iff_forall, forall_and]

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