infs_subset

Mathlib.Data.Finset.Sups

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

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 : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ ⊼ t₂ :=
  image₂_subset

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

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

Разделы

Аффилиация

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