set_prod_right — Mathlib

English

If t1 and t2 are disjoint, then for any s1, s2, the product sets s1 × t1 and s2 × t2 are disjoint.

Русский

Если t1 и t2 не пересекаются, то для любых s1, s2 множества s1 × t1 и s2 × t2 не пересекаются.

LaTeX

$$$ \text{Disjoint } t_1 t_2 \Rightarrow \forall s_1 s_2, \ \text{Disjoint} (s_1 \times t_1) (s_2 \times t_2) $$$

Lean4

theorem set_prod_right (ht : Disjoint t₁ t₂) (s₁ s₂ : Set α) : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) :=
  disjoint_left.2 fun ⟨_a, _b⟩ ⟨_, hb₁⟩ ⟨_, hb₂⟩ => disjoint_left.1 ht hb₁ hb₂

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