div_subset_div

Mathlib.Algebra.Group.Pointwise.Set.Basic

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

English

If s1 ⊆ t1 and s2 ⊆ t2, then s1 / s2 ⊆ t1 / t2.

Русский

Если s1 ⊆ t1 и s2 ⊆ t2, то s1 / s2 ⊆ t1 / t2.

LaTeX

$$$ s_1 \subseteq t_1 \rightarrow s_2 \subseteq t_2 \rightarrow s_1 / s_2 \subseteq t_1 / t_2 $$$

Lean4

@[to_additive (attr := mono, gcongr)]
theorem div_subset_div : s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ / s₂ ⊆ t₁ / t₂ :=
  image2_subset

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

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

Разделы

Аффилиация

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