prod_subset_prod_iff_right — 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).Nonempty \Rightarrow (s \times t = s_1 \times t_1 \iff s = s_1 \land t = t_1) $$$

Lean4

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

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