monovaryOn_const_right

Mathlib.Order.Monotone.Monovary

URI: https://scilib.ai/kg/mathlib#monovaryOn_const_right

English

MonovaryOn f (const ι b) s for any f, b, s.

Русский

MonovaryOn f (константная функция ι → β) s для любых f, b, s.

LaTeX

$$$\\operatorname{MonovaryOn}(f, \\operatorname{const}_{\\iota} b, s)$$$

Lean4

theorem monovaryOn_const_right (f : ι → α) (b : β) (s : Set ι) : MonovaryOn f (const ι b) s := fun _ _ _ _ h =>
  (h.ne rfl).elim

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

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

Разделы

Аффилиация

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