comp_continuousOn_iff — Mathlib

English

If e is an isometry, then ContOn of e ∘ f on s is equivalent to ContOn of f on s.

Русский

Если e — изометрия, то непрерывность на множестве сохраняется под композиции: ContOn(e ∘ f) = ContOn(f).

LaTeX

$$$\mathrm{ContinuousOn}(e \circ f, s) \iff \mathrm{ContinuousOn}(f, s)$$$

Lean4

@[simp]
theorem comp_continuousOn_iff {f : α → P} {s : Set α} : ContinuousOn (e ∘ f) s ↔ ContinuousOn f s :=
  e.isometry.comp_continuousOn_iff

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