outCLM_isUniformInducing — Mathlib

English

For every K and E with the given algebraic and uniform structures, the map outCLM K E is uniform-inducing.

Русский

Для любых K и E с указанными алгебраическими и равномерными структурами отображение outCLM K E является униформно-индукирующим.

LaTeX

$$$ \mathrm{IsUniformInducing}(\mathrm{outCLM}_{K,E}) $$$

Lean4

theorem outCLM_isUniformInducing : IsUniformInducing (outCLM K E) :=
  by
  rw [← isUniformInducing_mk.isUniformInducing_comp_iff, mk_comp_outCLM]
  exact .id

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