exists_forall_closedBall_subset_aux₂

English

For any y, the set of radii r such that closedBall y r ⊆ U_i whenever y ∈ K_i is convex; more precisely, the set Ioi(0) ∩ ⋂_{i: y ∈ K_i} {r | closedBall y r ⊆ U_i} is convex.

Русский

Для любой y множество радиусов r>0, удовлетворяющих условию y ∈ K_i ⇒ closedBall(y,r) ⊆ U_i, выпукло.

LaTeX

$$$\\text{Convex}_{\\\\mathbb{R}} \\\\big( Ioi(0) \\\\cap \\\\bigcap_{i: y \\in K_i} \\{ r \\\\mid closedBall(y,r) \\subseteq U_i \\} \\\\big)$$$

Lean4

theorem exists_forall_closedBall_subset_aux₂ (y : X) :
    Convex ℝ (Ioi (0 : ℝ) ∩ ENNReal.ofReal ⁻¹' ⋂ (i) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}) :=
  (convex_Ioi _).inter <|
    OrdConnected.convex <|
      OrdConnected.preimage_ennreal_ofReal <|
        ordConnected_iInter fun i =>
          ordConnected_iInter fun (_ : y ∈ K i) => ordConnected_setOf_closedBall_subset y (U i)

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