English
Let s, t1, t2, u be sets with decidable (Disjoint t1 t2). Then s × t1 ○ t2 × u equals ∅ if Disjoint, else s × u.
Русский
Пусть s, t1, t2, u — множества, имеющие decidable(Disjoint t1 t2). Тогда s × t1 ○ t2 × u равно ∅, если t1 и t2 непересекаются, иначе s × u.
LaTeX
$$s \times t_1 \circ t_2 \times u = \begin{cases} \emptyset & \text{if } Disjoint(t_1,t_2) \\ s \times u & \text{otherwise} \end{cases}$$
Lean4
theorem prod_comp_prod (s : Set α) (t₁ t₂ : Set β) (u : Set γ) [Decidable (Disjoint t₁ t₂)] :
s ×ˢ t₁ ○ t₂ ×ˢ u = if Disjoint t₁ t₂ then ∅ else s ×ˢ u :=
by
split_ifs with hst
· exact prod_comp_prod_of_disjoint hst ..
· rw [prod_comp_prod_of_inter_nonempty <| Set.not_disjoint_iff_nonempty_inter.1 hst]
