continuous_rng_of_principal — Mathlib

English

The continuous rng_of_principal equivalence asserts that continuity of f and of its composed coe are equivalent.

Русский

Соотношение непрерывности f и непрерывности композиции с coe.

LaTeX

$$Continuous f ⇔ Continuous (↑ ∘ f) for principal S.$$

Lean4

theorem continuous_rng_of_principal {X : Type*} [TopologicalSpace X] {f : X → Πʳ i, [R i, A i]_[𝓟 S]} :
    Continuous f ↔ Continuous ((↑) ∘ f : X → Π i, R i) :=
  isEmbedding_coe_of_principal.continuous_iff

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