English
For a map f: X → Mˣ, f is continuous iff the composed maps into M and the inverse-coordinate are continuous: val ∘ f and (u ↦ ↑(f(u))^{-1}) are both continuous.
Русский
Для отображения f: X → Mˣ выполнено: непрерывно тогда и только тогда, когда непрерывны comp(f, val) и (u ↦ ↑(f(u))^{-1}).
LaTeX
$$$\\text{Continuous}(f) \\iff \\text{Continuous}(\\mathrm{val} \\circ f) \\land \\text{Continuous}(\\lambda x, (f(x))^{-1})$$$
Lean4
@[to_additive]
protected theorem continuous_iff {f : X → Mˣ} :
Continuous f ↔ Continuous (val ∘ f) ∧ Continuous (fun x => ↑(f x)⁻¹ : X → M) := by
simp only [isInducing_embedProduct.continuous_iff, embedProduct_apply, Function.comp_def, continuous_prodMk,
opHomeomorph.symm.isInducing.continuous_iff, opHomeomorph_symm_apply, unop_op]
