monotone_restrict — Mathlib

English

Restriction is monotone with respect to the underlying prepartition order: if π1 ≤ π2 then π1.restrict J ≤ π2.restrict J.

Русский

Ограничение монотонно по отношению порядка предразбиения: если π1 ≤ π2, то π1.restrict J ≤ π2.restrict J.

LaTeX

$$$ (\\pi_1 \\le \\pi_2) \\Rightarrow (\\pi_1.restrict J \\le \\pi_2.restrict J) $$$

Lean4

theorem monotone_restrict : Monotone fun π : Prepartition I => restrict π J := fun _ _ => restrict_mono

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