singleton_infs_singleton

Mathlib.Data.Finset.Sups

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

English

The infimum of two singletons is the singleton of their infimum: {a} ⊼ {b} = {a ⊓ b}.

Русский

Инфинум двух одиночек равен одиночке их наименьшего элемента: {a} ⊼ {b} = {a ⊓ b}.

LaTeX

$$$ {a} \⊼ {b} = \{ a \wedge b \} $$$

Lean4

theorem singleton_infs_singleton : ({ a } ⊼ { b } : Finset α) = {a ⊓ b} :=
  image₂_singleton

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

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

Разделы

Аффилиация

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