prod_comp_prod_of_inter_nonempty

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.prod_comp_prod_of_inter_nonempty

English

If ht : (t1 ∩ t2).Nonempty, then s × t1 ○ t2 × u = s × u.

Русский

Если ht : (t1 ∩ t2).Nonempty, то s × t1 ○ t2 × u = s × u.

LaTeX

$$(t_1 \cap t_2).Nonempty \Rightarrow s \times t_1 \circ t_2 \times u = s \times u$$

Lean4

theorem prod_comp_prod_of_inter_nonempty (ht : (t₁ ∩ t₂).Nonempty) (s : Set α) (u : Set γ) :
    s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u := by aesop

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru