lebesgue_number_lemma_nhdsWithin — Mathlib

English

With nhdsWithin, compact K and a neighborhood mapping that targets K, there exists a basis index giving containment of balls into U.

Русский

С nhdsWithin, для компактного K и отображения окрестностей существует индекс базиса, обеспечивающий включение шаров в U.

LaTeX

$$$$\\exists i, p(i) \\wedge \\forall x \\in K, \\exists y, B(x,V_i) \\cap K \\subseteq U(y).$$$$

Lean4

protected theorem lebesgue_number_lemma_nhdsWithin {ι' : Sort*} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : α → Set α}
    (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ 𝓝[K] x) :
    ∃ i, p i ∧ ∀ x ∈ K, ∃ y, ball x (V i) ∩ K ⊆ U y :=
  by
  refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin hK hU)
  exact fun s t hst ht x hx ↦ (ht x hx).imp fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy

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