disjUnion — Mathlib

English

The tagged singleton is subordinate to r iff the corresponding Icc box is contained in the closed ball around x with radius r(x).

Русский

Помеченное одиночное разбиение подчинено радиусу r тогда и только тогда, когда соответствующая коробка Icc лежит внутри замкнутого шара вокруг x радиуса r(x).

LaTeX

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

Lean4

theorem disjUnion [Fintype ι] (h₁ : IsSubordinate π₁ r) (h₂ : IsSubordinate π₂ r) (h : Disjoint π₁.iUnion π₂.iUnion) :
    IsSubordinate (π₁.disjUnion π₂ h) r := by
  classical
  refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
  · rw [disjUnion_tag_of_mem_left _ hJ]
    exact h₁ _ hJ
  · rw [disjUnion_tag_of_mem_right _ hJ]
    exact h₂ _ hJ

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