comap_discreteTopology — Mathlib

English

If L is a Z-lattice and e is a continuous linear isomorphism, then ZLattice.comap K L e is a Z-lattice.

Русский

Если L — Z-решётка и e — непрерывное линейное изоморфизм, тогда ZLattice.comap K L e — Z-решётка.

LaTeX

$$$IsZLattice K (ZLattice.comap K L e.toLinearMap)$$$

Lean4

theorem comap_discreteTopology [hL : DiscreteTopology L] {e : F →ₗ[K] E} (he₁ : Continuous e)
    (he₂ : Function.Injective e) : DiscreteTopology (ZLattice.comap K L e) := by
  exact DiscreteTopology.preimage_of_continuous_injective L he₁ he₂

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