instMin

Mathlib.Order.Hom.Bounded

URI: https://scilib.ai/kg/mathlib#TopHom.instMin

English

The infimum in TopHom is defined pointwise: (f Ⓧ g)(a) = f(a) Ⓧ g(a).

Русский

На TopHom задаём наименьшее сверху точечно: (f ⊓ g)(a) = f(a) ⊓ g(a).

LaTeX

$$$(f \\wedge g)(a) = f(a) \\wedge g(a).$$$

Lean4

instance : Min (TopHom α β) :=
  ⟨fun f g => ⟨f ⊓ g, by rw [Pi.inf_apply, map_top, map_top, inf_top_eq]⟩⟩

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

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

Разделы

Аффилиация

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