infs_inter_subset_left

Mathlib.Data.Set.Sups

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

English

(S1 ∩ S2) ⊼ T ⊆ (S1 ⊼ T) ∩ (S2 ⊼ T).

Русский

Пересечение слева сохраняет включение: (S1 ∩ S2) ⊼ T ⊆ (S1 ⊼ T) ∩ (S2 ⊼ T).

LaTeX

$$$ (s_1 \cap s_2) \⊼ t \subseteq s_1 \⊼ t \cap s_2 \⊼ t $$$

Lean4

theorem infs_inter_subset_left : (s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t :=
  image2_inter_subset_left

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

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

Разделы

Аффилиация

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