union_div_inter_subset_union — Mathlib

English

Let s1,s2,t1,t2 be finite subsets of α with a division operation. Then the division by an intersection distributes over a union of the left-hand sides: (s1 ∪ s2) /(t1 ∩ t2) ⊆ (s1 / t1) ∪ (s2 / t2).

Русский

Пусть s1,s2,t1,t2 — конечные подмножества α с операцией деления. Тогда деление по пересечению делит объединение левых частей: (s1 ∪ s2) /(t1 ∩ t2) ⊆ (s1 / t1) ∪ (s2 / t2).

LaTeX

$$$$ (s_1 \\cup s_2) /(t_1 \\cap t_2) \\subseteq s_1 / t_1 \\cup s_2 / t_2 $$$$

Lean4

@[to_additive]
theorem union_div_inter_subset_union : (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂ :=
  image₂_union_inter_subset_union

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