antivaryOn_const_right

Mathlib.Order.Monotone.Monovary

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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