instDiscreteTopologySubtypeMemSubmoduleIntComap

English

If span K (L) is the whole space and L satisfies a range inclusion, then span K of ZLattice.comap K L e is the entire space.

Русский

Если span K (L) = ⊤ и L включено в диапазон e, то span K (ZLattice.comap K L e) = ⊤.

LaTeX

$$$\\text{span}_K(\\text{ZLattice.comap } K L e) = \\top$$$

Lean4

instance [DiscreteTopology L] (e : F ≃L[K] E) : DiscreteTopology (ZLattice.comap K L e.toLinearMap) :=
  ZLattice.comap_discreteTopology K L e.continuous e.injective

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