infs_left_comm

Mathlib.Data.Finset.Sups

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

English

Nested infima commute: s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v).

Русский

Вложенные инфимума коммутируют: s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v).

LaTeX

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

Lean4

theorem infs_left_comm : s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u) :=
  image₂_left_comm inf_left_comm

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

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

Разделы

Аффилиация

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