iSup_pair

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#iSup_pair

English

For f: β → α and a,b ∈ β, the supremum over {a,b} equals f(a) ⊔ f(b).

Русский

Для f: β → α и элементов a,b ∈ β супремум по {a,b} равен f(a) ⊔ f(b).

LaTeX

$$$$ \\sup_{x \\in \\{a, b\\}} f(x) = f(a) \\;\\sqcup\\; f(b) $$$$

Lean4

theorem iSup_pair {f : β → α} {a b : β} : ⨆ x ∈ ({ a, b } : Set β), f x = f a ⊔ f b := by
  rw [iSup_insert, iSup_singleton]

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

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

Разделы

Аффилиация

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