diffs_subset_left

Mathlib.Data.Finset.Sups

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

English

If t1 ⊆ t2, then s \\ t1 ⊆ s \\ t2.

Русский

Если t1 ⊆ t2, то s \\ t1 ⊆ s \\ t2.

LaTeX

$$$ t_1 \\subseteq t_2 \\to s \\\\ t_1 \\subseteq s \\\\ t_2 $$$

Lean4

theorem diffs_subset_left : t₁ ⊆ t₂ → s \\ t₁ ⊆ s \\ t₂ :=
  image₂_subset_left

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

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

Разделы

Аффилиация

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