div_inter_subset

Mathlib.Algebra.Group.Pointwise.Set.Basic

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

English

Division by the intersection of divisors: s / (t1 ∩ t2) ⊆ s / t1 ∩ (s / t2).

Русский

Деление на пересечение делителей: s / (t1 ∩ t2) ⊆ s / t1 ∩ (s / t2).

LaTeX

$$$ s / (t_1 \cap t_2) \subseteq s / t_1 \cap (s / t_2) $$$

Lean4

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

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

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

Разделы

Аффилиация

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