product_eq_univ

Mathlib.Data.Fintype.Prod

URI: https://scilib.ai/kg/mathlib#Finset.product_eq_univ

English

If s × t = univ then s = univ and t = univ (assuming nonempty α, β).

Русский

Если произведение s × t равно вселене, то s = univ и t = univ (при непустых α,β).

LaTeX

$$$s \\times\\! t = univ \\Rightarrow (s = univ \\land t = univ)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru