inf

Mathlib.Topology.ContinuousMap.Ordered

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

English

The infimum of two continuous maps is defined pointwise: (f ⊓ g)(a) = f(a) ⊓ g(a).

Русский

Инфимума двух непрерывных отображений определяется по точкам: (f ⊓ g)(a) = f(a) ⊓ g(a).

LaTeX

$$\$f,g:\\, C(α, β)\$ defined inf: (f \\sqcap g)(a) = f(a) \\sqcap g(a).$$

Lean4

instance inf : Min C(α, β) where min f g := { toFun := fun a ↦ f a ⊓ g a }

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

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

Разделы

Аффилиация

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