continuousOn_inv_iff — Mathlib

English

Let G be a topological group with continuous inversion. For every α and every f: α → G and every s ⊆ α, continuous on f⁻¹ on s is equivalent to continuous on f on s.

Русский

Пусть G — топологическая группа с непрерывной инверсией. Для каждого α, f: α → G и множества s ⊆ α верно, что ContinuousOn f⁻¹ s эквивалентно ContinuousOn f s.

LaTeX

$$$\forall f:\alpha \to G, \forall s\subseteq \alpha, \text{ContinuousOn}(f^{-1},s) \iff \text{ContinuousOn}(f,s).$$$

Lean4

@[to_additive (attr := simp)]
theorem continuousOn_inv_iff : ContinuousOn f⁻¹ s ↔ ContinuousOn f s :=
  (Homeomorph.inv G).comp_continuousOn_iff _ _

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