prod_subset_prod_iff_left — Mathlib

English

If the product s × t is nonempty, then s × t ⊆ s1 × t1 iff s ⊆ s1 ∧ t ⊆ t1.

Русский

Если произведение s × t непусто, то s × t ⊆ s1 × t1 эквивалентно s ⊆ s1 ∧ t ⊆ t1.

LaTeX

$$$ (s \times t) \subseteq (s_1 \times t_1) \iff (s \subseteq s_1 \land t \subseteq t_1) $ при условии $ (s \times t) \neq \emptyset $$$

Lean4

theorem prod_subset_prod_iff_left (h : t.Nonempty) : s ×ˢ t ⊆ s₁ ×ˢ t ↔ s ⊆ s₁ := by
  simp +contextual [prod_subset_prod_iff, or_iff_left h.ne_empty]

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