comp_antitone_on_left

Mathlib.Order.Monotone.Monovary

URI: https://scilib.ai/kg/mathlib#AntivaryOn.comp_antitone_on_left

English

If AntivaryOn f g s and f' is antitone, then MonovaryOn (f' ∘ f) g s.

Русский

Если AntivaryOn f g s и f' антитонна, то MonovaryOn (f' ∘ f) g s.

LaTeX

$$$\\operatorname{AntivaryOn}(f,g,s) \\rightarrow \\operatorname{Antitone}(f') \\rightarrow \\operatorname{MonovaryOn}(f' \\circ f, g, s)$$$

Lean4

theorem comp_antitone_on_left (h : AntivaryOn f g s) (hf : Antitone f') : MonovaryOn (f' ∘ f) g s :=
  fun _ hi _ hj hij => hf <| h hi hj hij

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

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

Разделы

Аффилиация

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