mono' — Mathlib

English

If r1 ≤ r2 pointwise after tagging, then subordinate property is preserved from r1 to r2.

Русский

Если r1(x) ≤ r2(x) для всех x после тегирования, то свойство подчинения сохраняется с r1 на r2.

LaTeX

$$$ \\forall J,\\; (\\pi.tag J) : r_1(\\pi.tag J) \\le r_2(\\pi.tag J) \\Rightarrow IsSubordinate(\\pi, r_2) $$$

Lean4

theorem mono' [Fintype ι] {π : TaggedPrepartition I} (hr₁ : π.IsSubordinate r₁)
    (h : ∀ J ∈ π, r₁ (π.tag J) ≤ r₂ (π.tag J)) : π.IsSubordinate r₂ := fun _ hJ _ hx =>
  closedBall_subset_closedBall (h _ hJ) (hr₁ _ hJ hx)

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