infs_union_left

Mathlib.Data.Set.Sups

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

English

(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 :=
  image2_union_left

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

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

Разделы

Аффилиация

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