ordConnected_setOf_ball_subset — Mathlib

English

For any x and s, the set { r | ball x r ⊆ s } is OrdConnected.

Русский

Для любых x и s множество { r | шар x r ⊆ s } является OrdConnected.

LaTeX

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

Lean4

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

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