exists_thickening_subset_open — Mathlib

English

If s is compact, t is open, and s ⊆ t, there exists δ > 0 with cthickening δ s ⊆ t.

Русский

Пусть s компактно, t открыто, s ⊆ t. Существует δ > 0 такое, что cthickening δ s ⊆ t.

LaTeX

$$$\\exists \\delta > 0:\\ \\mathrm{cthickening}_{\\delta}(s) \\subseteq t.$$$

Lean4

theorem _root_.IsCompact.exists_thickening_subset_open (hs : IsCompact s) (ht : IsOpen t) (hst : s ⊆ t) :
    ∃ δ, 0 < δ ∧ thickening δ s ⊆ t :=
  let ⟨δ, h₀, hδ⟩ := hs.exists_cthickening_subset_open ht hst
  ⟨δ, h₀, (thickening_subset_cthickening _ _).trans hδ⟩

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