one_le_thickenedIndicator_apply

Mathlib.Topology.MetricSpace.ThickenedIndicator

URI: https://scilib.ai/kg/mathlib#one_le_thickenedIndicator_apply

← MathLib Explorer

English

If x ∈ E, thickenedIndicator δ_pos E x = 1.

Русский

Если x ∈ E, thickenedIndicator δ_pos E x = 1.

LaTeX

$$$\forall δ>0,\; E:\; x \in E \Rightarrow \operatorname{thickenedIndicator}(δ,E)(x) = 1$$$

Lean4

theorem one_le_thickenedIndicator_apply (X : Type _) [PseudoEMetricSpace X] {δ : ℝ} (δ_pos : 0 < δ) {F : Set X} {x : X}
    (hxF : x ∈ F) : 1 ≤ thickenedIndicator δ_pos F x :=
  one_le_thickenedIndicator_apply' δ_pos (subset_closure hxF)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru