continuous_rng_of_top — Mathlib

English

Equivalence of continuous rng_of_top with the composition coe; the statement expresses a standard equivalence of continuity for the top principal case.

Русский

Эквивалентность непрерывности rng_of_top и композиции coe.

LaTeX

$$Continuous f ↔ Continuous (↑ ∘ f) for top principal case.$$

Lean4

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

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