diffs_subset

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.diffs_subset

English

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

Русский

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

LaTeX

$$$ s_1 \\subseteq s_2 \\to t_1 \\subseteq t_2 \\to s_1 \\\\ t_1 \\subseteq s_2 \\\\ t_2 $$$

Lean4

theorem diffs_subset : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ \\ t₁ ⊆ s₂ \\ t₂ :=
  image₂_subset

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

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

Разделы

Аффилиация

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