prod_comp_prod_of_disjoint — Mathlib

English

If t1 and t2 are disjoint, then s × t1 ○ t2 × u = ∅.

Русский

Если t1 и t2 не пересекаются, то s × t1 ○ t2 × u = пусто.

LaTeX

$$Disjoint(t_1,t_2) \Rightarrow s \times t_1 \circ t_2 \times u = \emptyset$$

Lean4

theorem prod_comp_prod_of_disjoint (ht : Disjoint t₁ t₂) (s : Set α) (u : Set γ) : s ×ˢ t₁ ○ t₂ ×ˢ u = ∅ :=
  Set.eq_empty_of_forall_notMem fun _ ⟨_z, ⟨_, hzs⟩, hzu, _⟩ ↦ Set.disjoint_left.1 ht hzs hzu

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