comp

Mathlib.Order.Monotone.Defs

URI: https://scilib.ai/kg/mathlib#StrictAnti.comp

English

If g is StrictAnti and f is StrictAnti, then g ∘ f is StrictMono.

Русский

Если g и f StrictAnti, то композиция g ∘ f StrictMono.

LaTeX

$$StrictAnti g ∧ StrictAnti f ⇒ StrictMono (g ∘ f)$$

Lean4

protected theorem comp (hg : StrictAnti g) (hf : StrictAnti f) : StrictMono (g ∘ f) := fun _ _ h ↦ hg (hf h)

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

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

Разделы

Аффилиация

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