monotone_accumulate — Mathlib

English

If x ≤ y then Accumulate s x ⊆ Accumulate s y; i.e., the map x ↦ Accumulate s x is monotone with respect to ≤ on α.

Русский

Если x ≤ y, то Accumulate s x ⊆ Accumulate s y; функция x ↦ Accumulate s x монотоне относительно ≤ на α.

LaTeX

$$$\\text{Monotone}(\\mathrm{Accumulate}(s), x, y) \\text{ whenever } x \\le y$$$

Lean4

theorem monotone_accumulate [Preorder α] : Monotone (Accumulate s) := fun _ _ hxy =>
  biUnion_subset_biUnion_left fun _ hz => le_trans hz hxy

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