infs_union_left

Mathlib.Data.Finset.Sups

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

English

Infimum distributes over union on the left: (S1 ∪ S2) ⊼ T = (S1 ⊼ T) ∪ (S2 ⊼ T).

Русский

Инфинум распределяется над объединением слева: (S1 ∪ S2) ⊼ T = (S1 ⊼ T) ∪ (S2 ⊼ T).

LaTeX

$$$ (S_1 \cup S_2) \⊼ T = (S_1 \⊼ T) \cup (S_2 \⊼ T) $$$

Lean4

theorem infs_union_left : (s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t :=
  image₂_union_left

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

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

Разделы

Аффилиация

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