thickening_subset_cthickening — Mathlib

English

For any δ and E, cthickening δ E equals the preimage of (−∞, δ] under infEdist(·, E).

Русский

Для любых δ и E cthickening δ E равно предобразу множества (−∞, δ] под infEdist(ъ, E).

LaTeX

$$$ cthickening δ E = infEdist^{-1}((-\infty, δ]) $$$

Lean4

/-- The open thickening `Metric.thickening δ E` is contained in the closed thickening
`Metric.cthickening δ E` with the same radius. -/
theorem thickening_subset_cthickening (δ : ℝ) (E : Set α) : thickening δ E ⊆ cthickening δ E :=
  by
  intro x hx
  rw [thickening, mem_setOf_eq] at hx
  exact hx.le

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