English
If a function f defines an induced topology on α from β, and β has continuous inversion, then α has a continuous inversion with respect to the induced topology.
Русский
Если f задаёт понятие индуцированной топологии на α от β, и в β непрерывно обратимое, то на α непрерывно обратимо относительно индуцированной топологии.
LaTeX
$$$\\text{ContinuousInv}(α)\\text{ for }(t_β\\text{ induced by }f).$$$
Lean4
@[to_additive]
theorem induced {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [Group α] [DivisionMonoid β] [MonoidHomClass F α β]
[tβ : TopologicalSpace β] [ContinuousInv β] (f : F) : @ContinuousInv α (tβ.induced f) _ :=
by
let _tα := tβ.induced f
refine ⟨continuous_induced_rng.2 ?_⟩
simp only [Function.comp_def, map_inv]
fun_prop
