const

Mathlib.Order.Hom.Lattice

URI: https://scilib.ai/kg/mathlib#SupHom.const

Lean4

/-- The constant function as a `SupHom`. -/
def const (b : β) : SupHom α β :=
  ⟨fun _ ↦ b, fun _ _ ↦ (sup_idem _).symm⟩

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

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

Разделы

Аффилиация

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