inter_div_union_subset_union — Mathlib

English

The division distributes over union inside the denominator: s1 ∩ s2 / (t1 ∪ t2) ⊆ s1 / t1 ∪ s2 / 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₂ :=
  image2_inter_union_subset_union

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