mono — Mathlib

English

If π is subordinate to r1 and r1 ≤ r2 pointwise on boxes, then π is subordinate to r2.

Русский

Если π подчинено r1 и r1 по каждому x не больше чем r2, то π подчинено r2.

LaTeX

$$$ IsSubordinate(\\pi, r_1) \\land \\forall x, x \\in \\mathrm{Icc} \\Rightarrow r_1(x) \\le r_2(x) \\Rightarrow IsSubordinate(\\pi, r_2) $$$

Lean4

theorem mono [Fintype ι] {π : TaggedPrepartition I} (hr₁ : π.IsSubordinate r₁) (h : ∀ x ∈ Box.Icc I, r₁ x ≤ r₂ x) :
    π.IsSubordinate r₂ :=
  hr₁.mono' fun J _ => h _ <| π.tag_mem_Icc J

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