inter_div_union_subset_union — Mathlib

English

Let s1,s2,t1,t2 be finite subsets of α with a binary operation defined. Then the division by a union distributes over the union of divisions: (s1 ∩ s2) /(t1 ∪ t2) ⊆ (s1 / t1) ∪ (s2 / t2).

Русский

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

LaTeX

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

Lean4

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

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