infs_subset_left

Mathlib.Data.Finset.Sups

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

English

If t1 ⊆ t2 then s ⊼ t1 ⊆ s ⊼ t2.

Русский

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

LaTeX

$$$ t_1 \subseteq t_2 \rightarrow s ⊼ t_1 \subseteq s ⊼ t_2 $$$

Lean4

theorem infs_subset_left : t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂ :=
  image₂_subset_left

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

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

Разделы

Аффилиация

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