semilatticeInf

Mathlib.Topology.ContinuousMap.Ordered

URI: https://scilib.ai/kg/mathlib#ContinuousMap.semilatticeInf

English

There is a SemilatticeInf structure on C(α, β) given by pointwise infimum.

Русский

На пространстве непрерывных отображений C(α, β) введено инфиминум по точкам.

LaTeX

$$\$SemilatticeInf\\, C(α, β)\$$$

Lean4

instance semilatticeInf : SemilatticeInf C(α, β) :=
  DFunLike.coe_injective.semilatticeInf _ fun _ _ ↦ rfl

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

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

Разделы

Аффилиация

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