inter_div_subset

Mathlib.Algebra.Group.Pointwise.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.inter_div_subset

English

The division distributes over intersection on the numerator side: (s1 ∩ s2) / t ⊆ (s1 / t) ∩ (s2 / t).

Русский

Деление по пересечению по числителю распределяется: (s1 ∩ s2) / t ⊆ (s1 / t) ∩ (s2 / t).

LaTeX

$$$ (s_1 \cap s_2) / t \subseteq (s_1 / t) \cap (s_2 / t) $$$

Lean4

@[to_additive]
theorem inter_div_subset : s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t) :=
  image2_inter_subset_left

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

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

Разделы

Аффилиация

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