Theorems · Theorem · order theory

Set.prod_subset_prod_iff

∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β}, s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

A product set is included in a product set if and only factors are included, or a factor of the first set is empty.

Defined in

Mathlib.Data.Set.Prod

Cited by

15 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound