instIsZLatticeComap — Mathlib

English

For x ∈ L, the comap_equiv map sends x to e.symm x.

Русский

Для x ∈ L отображение comap_equiv отправляет x в e.symm x.

LaTeX

$$$ZLattice.comap_equiv K L e x = e^{-1}(x) \\quad (x \\in L)$$$

Lean4

instance instIsZLatticeComap [DiscreteTopology L] [IsZLattice K L] (e : F ≃L[K] E) :
    IsZLattice K (ZLattice.comap K L e.toLinearMap) where
  span_top := by
    rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, LinearEquivClass.range]

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