comap_refl — Mathlib

English

If L is discrete and e is a continuous linear map, then the pulled-back lattice ZLattice.comap K L e is discrete.

Русский

Если L дискретна и e — непрерывное линейное отображение, тогда решётка, полученная через comap, дискретна.

LaTeX

$$$\\text{DiscreteTopology}(L) \\Rightarrow \\text{DiscreteTopology}(ZLattice.comap K L e)$$$

Lean4

theorem comap_refl : ZLattice.comap K L (1 : E →ₗ[K] E) = L :=
  Submodule.comap_id L

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