sup_apply

Mathlib.Topology.ContinuousMap.Ordered

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

English

The coercion commutes with the pointwise infimum: the evaluation of f ⊓ g is the infimum of the evaluations.

Русский

Приведение к функциям сохраняет операцию взятия нижнего предела: (f ⊓ g)(x) = f(x) ⊓ g(x).

LaTeX

$$$\\uparrow( f \\sqcap g) = \\uparrow f \\sqcap \\uparrow g$.$$

Lean4

@[simp]
theorem sup_apply (f g : C(α, β)) (a : α) : (f ⊔ g) a = f a ⊔ g a :=
  rfl

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

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

Разделы

Аффилиация

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