infs_assoc

Mathlib.Data.Finset.Sups

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

English

The infimum is associative: s ⊼ t ⊼ u = s ⊼ (t ⊼ u).

Русский

Инфинум ассоциативен: s ⊼ t ⊼ u = s ⊼ (t ⊼ u).

LaTeX

$$$ s \⊼ t \⊼ u = s \⊼ (t \⊼ u) $$$

Lean4

theorem infs_assoc : s ⊼ t ⊼ u = s ⊼ (t ⊼ u) :=
  image₂_assoc inf_assoc

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

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

Разделы

Аффилиация

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