isSubordinate_single — Mathlib

English

The singleton prepartition is subordinate to the radius function r iff Box.Icc(J) is contained in the closed ball around x with radius r(x).

Русский

Единичное предразбиение подчинено радиусу r тогда и только тогда, когда Icc(J) ⊆ замкнутый шар вокруг x радиуса r(x).

LaTeX

$$$ IsSubordinate (single I J hJ x h) \\; r \iff Box.Icc J \subseteq \overline{B}(x, r(x)) $$$

Lean4

@[simp]
theorem isSubordinate_single [Fintype ι] (hJ : J ≤ I) (h : x ∈ Box.Icc I) :
    IsSubordinate (single I J hJ x h) r ↔ Box.Icc J ⊆ closedBall x (r x) :=
  forall_mem_single (fun x J => Box.Icc J ⊆ closedBall x (r x)) hJ h

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