continuous_congr_of_inseparable — Mathlib

English

If for every x, f x is inseparable from g x, then f is continuous iff g is continuous.

Русский

Если для каждой x выполняется неразделимость f(x) и g(x), то f и g либо обе непрерывны, либо обе непрерывны не являются.

LaTeX

$$Continuous f ↔ Continuous g$$

Lean4

theorem continuous_congr_of_inseparable (h : ∀ x, f x ~ᵢ g x) : Continuous f ↔ Continuous g :=
  by
  simp_rw [SeparationQuotient.isInducing_mk.continuous_iff (Y := Y)]
  exact continuous_congr fun x ↦ SeparationQuotient.mk_eq_mk.mpr (h x)

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