ordConnected_setOf_closedBall_subset

English

For any x and s, the set of radii r such that the closed ball centered at x with radius r is contained in s is an ordinally connected subset of ℝ≥0∞.

Русский

Для любых x и s множество радиусов r, для которых замкнутый шар с центром x и радиусом r содержится в s, является ориентированно связным подмножеством ℝ≥0∞.

LaTeX

$$$\\operatorname{OrdConnected}\\{ r : \\mathbb{R}_{\\ge 0}^{\\infty} \\mid \\overline{\\mathrm{B}}(x,r) \\subseteq s \\}$$$

Lean4

theorem ordConnected_setOf_closedBall_subset (x : α) (s : Set α) : OrdConnected {r | closedBall x r ⊆ s} :=
  ⟨fun _ _ _ h₁ _ h₂ => (closedBall_subset_closedBall h₂.2).trans h₁⟩

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