mulIndicator — Mathlib

English

If hs encodes that f equals 1 on the frontier of s, and f is continuous, then the indicator-like function mulIndicator s f is continuous.

Русский

Если условие hs задаёт, что f равно 1 на границе множества s, и f непрерывна, то функция mulIndicator s f непрерывна.

LaTeX

$$$\\text{Continuous}(\\text{mulIndicator } s f)$$$

Lean4

@[to_additive]
protected theorem mulIndicator (hs : ∀ a ∈ frontier s, f a = 1) (hf : Continuous f) : Continuous (mulIndicator s f) :=
  by classical exact hf.piecewise hs continuous_const

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