indicator — Mathlib

English

The indicator of a clopen set yields a bounded continuous real-valued function.

Русский

Индикатор клэпного множества даёт ограниченно непрерывное отображение в ℝ.

LaTeX

$$$\\operatorname{indicator}(s,hs) \\in \\operatorname{BoundedContinuousFunction} \\alpha \\mathbb{R}$$$

Lean4

/-- The indicator function of a clopen set, as a bounded continuous function. -/
@[simps]
noncomputable def indicator (s : Set α) (hs : IsClopen s) : BoundedContinuousFunction α ℝ
    where
  toFun := s.indicator 1
  continuous_toFun := continuous_indicator (by simp [hs]) <| continuous_const.continuousOn
  map_bounded' := ⟨1, fun x y ↦ by by_cases hx : x ∈ s <;> by_cases hy : y ∈ s <;> simp [hx, hy]⟩

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