prod_self_subset_prod_self — Mathlib

English

The self-subset relation for product sets is equivalent to the componentwise subset relation: s1 × s1 ⊆ s2 × s2 iff s1 ⊆ s2.

Русский

Относительное отношение подмножеств для произведения в паре эквивалентно покомпонентному: s1 × s1 ⊆ s2 × s2 ⇔ s1 ⊆ s2.

LaTeX

$$@[simp] (s1 × s1 ⊆ s2 × s2) ↔ (s1 ⊆ s2)$$

Lean4

@[simp]
theorem prod_self_subset_prod_self : s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂ ↔ s₁ ⊆ s₂ :=
  ⟨fun h _ hx => (h (mk_mem_prod hx hx)).1, fun h _ hx => ⟨h hx.1, h hx.2⟩⟩

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