prod_subset_prod_iff' — Mathlib

English

A product is contained in another product iff componentwise inclusion holds or one side is empty.

Русский

Произведение содержится в другом произведении тогда и только тогда, когда выполняется поэлементное включение или одна сторона пуста.

LaTeX

$$$ s \times t \subseteq s_1 \times t_1 \iff (s \subseteq s_1 \land t \subseteq t_1) \lor (s = \emptyset \lor t = \emptyset) $$$

Lean4

theorem prod_subset_prod_iff' (h : (s ×ˢ t).Nonempty) : s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ :=
  by
  rw [prod_subset_prod_iff, or_iff_left]
  rw [← Set.prod_eq_empty_iff]
  exact h.ne_empty

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