continuous_mulIndicator — Mathlib

English

If s is clopen (both closed and open) and f is continuous, then s.mulIndicator f is continuous.

Русский

Если s открыто и замкнуто одновременно и f непрерывна, то s.mulIndicator f непрерывна.

LaTeX

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

Lean4

@[to_additive]
theorem continuous_mulIndicator (hs : IsClopen s) (hf : Continuous f) : Continuous (s.mulIndicator f) :=
  hf.mulIndicator (by simp [isClopen_iff_frontier_eq_empty.mp hs])

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