empty_sups

Mathlib.Data.Finset.Sups

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

English

The left supremum of the empty set with t is empty: ∅ ⊻ t = ∅.

Русский

Левая сумма пустого множества с t равна пустому: ∅ ⊻ t = ∅.

LaTeX

$$$ \varnothing \oplus t = \varnothing $$$

Lean4

@[simp]
theorem empty_sups : ∅ ⊻ t = ∅ :=
  image₂_empty_left

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

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

Разделы

Аффилиация

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